 \documentclass[preprint,11pt]{elsarticle}
 
\usepackage{intestazione2}
\usepackage[hide]{todo}
\usepackage{macron}
\usepackage{geometry}

\usepackage{times}
\usepackage{mathpartir}

\newcommand{\jtodo}[2]{\todo[\red{#1}]{#2}}  

\begin{document}
 
\begin{frontmatter}
\title{Disciplined Structured Communications with \\ 
%Consistent
Disciplined Runtime Adaptation}
%\title{Disciplined Adaptation for Structured Communications}
\author[evry]{Cinzia Di Giusto} 
\author[jbi]{Jorge A. P\'{e}rez}

%\cortext[cor1]{Corresponding author}  
\address[evry]{Universit\'e d'Evry - Val d'Essonne, Laboratoire IBISC}
%\address[unl]{CITI and Departamento de Inform\'atica, FCT Universidade Nova de Lisboa}
\address[jbi]{Johann Bernoulli Institute for Mathematics and Computer Science, University of Groningen}

   

\begin{abstract}
\emph{Session types} offer a powerful type-the\-o\-ret\-ic foundation for the analysis of 
structured communications, as commonly found in serv\-ice-oriented systems.
They are defined upon core programming calculi which offer only limited support 
for expressing %adaptation and evolvability 
requirements
related to \emph{runtime adaptation}.
This is unfortunate, as serv\-ice\--ori\-ented systems are increasingly being deployed upon 
highly dynamic infrastructures in which such requirements are 
central concerns.
In previous work, we developed a process calculi framework of \emph{adaptable processes},
in which concurrent processes can be replaced,  suspended, or discarded at runtime.
In this paper, we 
propose a session type discipline\done\todo[B33.]{Fixed here, need to check remaining occurrences of "session types disciplines".} for a calculus with adaptable processes. 
Our typed framework offers a simple alternative for integrating runtime adaptation mechanisms in 
the modeling and analysis of structured communications.
We show that 
well-typed processes enjoy \emph{safety} and \emph{consistency} properties:
while the former property ensures the absence of communication errors at runtime, the latter
guarantees that active session behavior is never disrupted by adaptation actions.\done\todo[B21]{Modified sentence, please check}
\end{abstract}

\end{frontmatter}



%\todo{TO DO:
%\begin{itemize}
%%\item definition and proof of consistency; harmonize presentation with safety
%%\item extend example?
%%\item say something about linear/single process variables?
%%\item we have no restriction on names... i can't recall why
%%\item alternative typing rules for adaptation for process with open sessions
%%\item interface compatibility
%%\item extended comparisons with session types with exceptions
%\item comparisons with the version in SAC'13
%\end{itemize}
%}

\section{Introduction}

\emph{Session types} 
offer a powerful type-theoretic foundation
for the analysis of 
complex 
scenarios of structured communications, as frequently found in service-oriented systems.  
They abstract communication protocols as basic interaction patterns, which 
may then be %are then statically 
checked against specifications\done\todo[C11.]{Fixed (dropped statically), pls check.}
in some core programming calculus ---typ\-i\-cal\-ly, a variant of the $\pi$-calculus~\cite{DBLP:journals/iandc/MilnerPW92a}. 
Introduced in~\cite{DBLP:conf/concur/Honda93,DBLP:conf/esop/HondaVK98}, 
session type theories 
%have received much attention and 
have been extended in multiple directions 
%two notable such extensions concern asynchronous and multiparty communications~(see, e.g.,~\cite{DBLP:conf/forte/KouzapasYH11} and~\cite{DBLP:conf/popl/HondaYC08}, respectively).
%(
---see~\cite{DBLP:conf/wsfm/Dezani-Ciancaglinid09} for a 
%detailed 
survey.
\done\todo[A5.]{Here we have mentioned extensions of session types, such as asynchronous
\cite{DBLP:conf/forte/KouzapasYH11} 
and multiparty
\cite{DBLP:conf/popl/HondaYC08}, as requested by the reviewer.}Their 
%The
practical relevance 
%of session types 
is witnessed by, e.g., 
 their 
 successful 
 application to the analysis of 
 %parallel programs~\cite{DBLP:conf/tools/NgYH12}.
 collaborative, distributed workflows in healthcare services~\cite{DBLP:conf/fhies/HenriksenNHYH12}.

In spite of these developments, 
we find that existing process frameworks based on ses\-sion types
do not adequately support 
%for reasoning about 
mechanisms for 
\emph{runtime adaptation}. 
%Adaptation and evolvability are increasingly relevant issues nowadays, 
%Runtime adaptation is an increasingly relevant issue nowadays, 
As distributed systems and applications are  being deployed in
open, highly dynamic infrastructures (such as cloud computing platforms),
%In such settings,  
runtime adaptation %and dynamic reconfiguration  
appears as a key feature to
ensure continued system operation,
reduce costs, and achieve
business agility.\done\todo[A4.]{J: We have expanded a bit on what we mean by runtime adaptation, but without using~\cite{DBLP:conf/fase/BruniCGLV12} as a reference.}
%More precisely, w
We understand runtime adaptation 
as the dynamic modification of (the behavior of) the system  %residing in a distinguished location 
as a response to an exceptional external event. %, external to the system. 
Even if such events may not be catastrophic, they are often hard to predict.
The initial system specification must explicitly describe the sub-systems amenable to adaptation and their exceptional events. 
Then, on the basis of this initial specification and its projected evolution, 
an array of possible  adaptation routines is defined at design time. 
Runtime adaptation then denotes potential behavior, in the sense that 
a given adaptation routine is triggered only if its associated exceptional event takes place.
While channel mobility  %~\cite{DBLP:journals/entcs/YoshidaV07}) 
present in session languages (commonly referred to as \emph{delegation})
is useful to specify distribution of processing via types~\cite{DBLP:conf/esop/HondaVK98}, 
%dynamic reconfiguration, 
we find that runtime adaptation, %, evolvability, and code update
%are not expressible or are 
in the sense just discussed, 
is hard to specify and reason about in those languages.\done\todo[A2.]{J: We have relaxed this sentence.}


%%possibility of dynamically replacing the behavior of a located process with a new session process that is in some sense ``compatible'' with the old behavior.
%the enhancement of process specifications with update routines which contain information for  potentially enabling reconfiguration actions at runtime. 
%While the information for such routines can be anticipated, 
%the exact conditions and timing for such actions cannot be fully predicted, but it is important to ensure that the code embedded in such update is well-typed.


We thus observe %a rather unfortunate discrepancy
a substantial gap\done\todo[A3.]{J: It was "a rather unfortunate discrepancy"} between 
(i)~the adaptation capabilities of %modern 
communication-based systems in practice, and 
(ii)~the forms of interaction available in existing
%the calculi upon which session types disciplines are defined.
(typed) process frameworks developed to reason about the correctness of such systems.


In this paper we propose an alternative for 
%elementary approach to 
filling in this gap. 
%overcome this discrepancy.
We %extend an existing 
introduce a
session type discipline 
for a language
equipped
with 
mechanisms for runtime adaptation.
Rather than developing yet another session type discipline \emph{from scratch}, we have deliberately 
preferred to build upon existing lines of work. 
Our proposal 
builds upon
%results from combining 
the framework of 
\emph{adaptable processes}, 
an attempt for enhancing process calculi specifications with evolvability mechanisms
which we have developed together with Bravetti and Zavattaro in~\cite{BGPZFMOODS}.
We combine the constructs for adaptable processes with
the main insights %principles %underlying the discipline 
of the session type system
put forward by Garralda et al.~\cite{DBLP:conf/ppdp/GarraldaCD06} for the Boxed Ambient calculus~\cite{DBLP:journals/toplas/BugliesiCC04}.
Since the type system in~\cite{DBLP:conf/ppdp/GarraldaCD06} does not support delegation, 
we incorporate this useful mechanism by relying on the ``liberal'' typing system developed by 
Yoshida and Vasconcelos in~\cite{DBLP:journals/entcs/YoshidaV07}.
As a result of this integration of concepts, 
we obtain a simple yet expressive model 
of structured communications with explicit mechanisms for runtime adaptation.


We briefly describe our approach and results. 
Our process language includes
the usual $\pi$-calculus constructs for session communication, but extended 
with the \emph{located processes} and the \emph{update processes} introduced in~\cite{BGPZFMOODS}.
Given a location $l$, a process $P$, and a context $Q$ 
(i.e. a process with zero or more free occurrences of variable $\mathsf{X}$), these two processes are noted $l[P]$ and 
$\adapt{l}{Q}{\mathsf{X}}$, respectively\done\todo[B1.]{The reviewer suggests to change this notation, using abstractions. We have used the notation for abstractions in Davide's book.}. 
%$l\{Q(\mathsf{X})\}$, resp. 
They may synchronize on $l$ so as to evolve into process 
$Q\subst{P}{\mathsf{X}}$ ---the process $Q$ in which all free occurrences of $\mathsf{X}$ are replaced with $P$.
This interaction represents the \emph{update} of  process $P$ at $l$ with an \emph{adaptation routine}
embodied by $Q$, thus realizing the vision of runtime adaptation hinted at above. 
Locations can be nested and are transparent:
within $l[P]$, process $P$ may evolve autonomously, with the potential of interacting with some %neighboring 
update process for $l$. 
%Context $Q$ can be seen as a built-in adaptation mechanism.
%$l\{Q(\mathsf{X})\}$, 
%$\adapt{l}{Q}{X}$,
%as just described, 

%Hence, 
In our language communicating behavior coexists with update actions. 
This raises the need for disciplining both forms of interaction, in  a way such that protocol abstractions\done\todo[B22.]{I think this doesn't apply}
 given by session types are respected and  evolvability requirements are enforced. 
To this end, by observing that %exploiting the fact that 
our update actions are a simple form of (higher-order) process mobility~\cite{San923}, 
we draw inspiration from the session types 
in~\cite{DBLP:conf/ppdp/GarraldaCD06}, 
which ensure that
sessions within Ambient hierarchies %are \emph{safe}, i.e., they 
are never disrupted by Ambient mobility steps.
By generalizing this insight to the context of (session) processes which execute
in arbitrary, possibly nested locations, we obtain a property which we call \emph{consistency}:
update actions over located processes which are engaged in active session behavior cannot be enabled.

%While both Ambients and adaptable processes rely on nested located processes,
%Ambient mobility and evolvability steps are conceptually very different.
%In fact, %is a major difference:
%Ambient mobility is only defined in a parent-child style, whereas
%located processes and update actions 
% may interact independently of their relative position in the hierarchy induced by location nesting.
%This way, integrating our calculus for adaptable processes %of~\cite{BGPZFMOODS} 
%with the session types discipline in~\cite{DBLP:conf/ppdp/GarraldaCD06}
%roughly amounts to: 

To show how
located and update processes fit in a session-typed process language, 
and to illustrate our  notion of consistency, 
let us 
consider a simple distributed client/server scenario,
% of distributed, interacting services (a client $C_1$ and a replicated service $S$), 
conveniently represented as located processes:
\begin{eqnarray*}
\mathsf{Sys} & \triangleq &  %\scomponent{l_{0}}{C_1} \para 
\scomponent{l_{1}}{C_1} \para\bigscomponent{l_2}{\scomponent{r}{S} \para R \, } \quad\text{where:} \vspace{3mm} \\ 
C_1  &  \triangleq  & \nopenr{a}{x}.\outC{x}{\mathrm{u_1},\mathrm{p_1}}.\select{x}{n_1.P_1}.\close{x} \\
S  &  \triangleq  & \repopen{a}{y}.\inC{y}{u,p}.\branch{y}{n_1{:}Q_1.\close{y}  \alte n_2{:}Q_2.\close{y}}
\end{eqnarray*}
Intuitively, 
$\mathsf{Sys}$ 
consists of a replicated server $S$ and a client $C_1$, hosted in different locations $r$ and $l_1$, respectively.\done\todo[B23.]{Changed order of $r$ and $l_1$, check.}
Process  $R$, in location $l_2$, represents the platform in which  $S$ is deployed.
The client $C_1$ and the (persistent) server $S$ may synchronize on name $a$ to establish a new session. %of type $\sigma$ 
%between $S$ and $C_1$ %($i \in \{0, 1\}$) 
After that,  
the client first sends its credentials to the server; then, she chooses\done\todo[B24.]{Fixed, although not in the way suggested.} one of the two
labeled alternatives offered by the server. 
Above, 
client $C_1$ selects the alternative on label $n_1$; 
the subsequent client and server behaviors are  abstracted by processes $P_1$ and $Q_1$, respectively.
%(resp. $P_1$ and $Q_1$), 
%which are left unspecified.
Finally, server and client synchronize to close the session.


Starting from $\mathsf{Sys}$, let us suppose that a new session is indeed established by a synchronization on $a$. 
The semantics of our process model decrees 
a reduction step $\mathsf{Sys} \pired \mathsf{Sys}'$:
%the following reduction step:  %We then have
\begin{eqnarray*}
\mathsf{Sys}' \!\!\!& = & \!\!\!\! (\nu \kappa)\big(\scomponent{l_{1}}{\outC{\kappa^{+}}{\mathrm{u_1},\mathrm{p_1}}.\select{\kappa^{+}}{n_1.P_1}.\close{\kappa^{+}}} \para \\ 
& & \qquad \bigscomponent{l_2}{\scomponent{r}{\inC{\kappa^{-}}{u,p}.\branch{\kappa^{-}}{n_1{:}Q_1.\close{\kappa^{-}} \alte n_2{:}Q_2.\close{\kappa^{-}}}\,} \para R \, }\big)
\end{eqnarray*} 
where 
$\kappa^+$ and $\kappa^-$ denote the two \emph{end-points} of channel $\kappa$~\cite{DBLP:journals/acta/GayH05}.
Suppose now that $R$ simply represents an upgrade process, which is ready to synchronize with $r$, the location in which $S$ resides: 
%$$R = \adaptn{r}{NewS(\mathsf{X})}$$
$$R = \adapt{r}{NewS}{\mathsf{X}}$$
From $\mathsf{Sys}'$, an update on $r$ would be  highly inconvenient for at least two reasons:
\begin{enumerate}[(a)]
\item First, since $r$ contains the local server behavior for an already established session, 
a careless update action on $r$ could potentially discard such behavior. This would leave the client in $l_1$ without a partner---the  protocol agreed upon session establishment would not be respected. 
\item Second, since $r$ contains also the actual service definition $S$, an undisciplined 
update action on $r$ could 
affect the service on $a$ in a variety of ways---for instance, it could destroy it. 
This clearly goes against the expected nature of services, which should be always available. 
\end{enumerate}

\noindent Above, item (a) concerns our intended notion of consistency, which ensures that any update actions on $r$
(such as those involving $R$ above) are only enabled  when $r$ contains no active sessions. 
Closely related, item (b) concerns a most desirable principle for services, namely that ``services should always be available in multiple copies''---this is the Service Channel Principle (SCP) identified in~\cite{DBLP:conf/esop/CarboneHY07}.


\paragraph{Contributions} The main contribution of this paper is a session typed framework with runtime adaptation.
 Our framework lies upon two main technical ingredients:
\begin{enumerate}[(1)]
%\item generalizing the operational semantics of~\cite{DBLP:conf/ppdp/GarraldaCD06}
%so as to account for adaptation in \emph{arbitrary process hierarchies}; 
\item An \emph{operational semantics} for  our session language with located and update processes~\cite{BGPZFMOODS}.
The semantics enables adaptation actions within  \emph{arbitrary process hierarchies} and, following~\cite{DBLP:conf/ppdp/GarraldaCD06}, 
endows each located process with a suitable \emph{runtime annotation}, which describes its active session behavior.
Runtime annotations for locations are key in avoiding undesirable update actions such as the described in~(a) above.

%conservatively extending the typing system in~\cite{DBLP:conf/ppdp/GarraldaCD06}, so as to be able to reason about \emph{process interfaces}.
\item A \emph{typing system} which extends existing session type systems~\cite{DBLP:journals/entcs/YoshidaV07,DBLP:conf/ppdp/GarraldaCD06}
with the notion of \emph{interface}, which allows\done\todo[B25.]{Fixed. Please check} for simple and intuitive static checking rules for evolvability constructs. 
In particular, interfaces are essential to rule out careless updates such as the described in (b) above.
This typing system provides a static analysis technique for ensuring not only
\emph{safety}\done\todo[B26.]{Fixed, please check}, i.e., absence of communication errors at runtime, but also 
consistency, as described above.
\end{enumerate}

%Ultimately, this last step is what realizes a form of \emph{typeful adaptation}, which contrasts with the untyped adaptation in~\cite{BGPZFMOODS}.  Well-typed processes 
%in our framework
%satisfy basic correctness guarantees (formalized as a Subject Reduction result), 
%which entails consistency for session-typed processes %that
%with runtime adaptation mechanisms.
%
%\jp{Perhaps adding an example of 'wrong' updates/consistency, to be addressed via static analysis?}


%\jp{This paragraph fits better at the end...}

\noindent To the best of our knowledge, our framework is the first in amalgamating structured communications and runtime adaptation from a session types perspective (either binary or multiparty).

\paragraph{Organization}
%The paper is structured as follows.
%Next, in \S\,\ref{sec:syn}, we 
The following section introduces our process language, a fairly standard session $\pi$-calculus extended with adaptable processes.
In \S\,\ref{s:types} our session type system is presented; 
its main properties, namely  safety and consistency, 
are defined and investigated in~\S\,\ref{sec:res}. 
The typed approach is illustrated via examples in~\S\,\ref{sec:exam}, where the client/server scenario discussed above is revisited.
Extensions and enhancements for our framework are discussed in~\S\,\ref{sec:disc}:
they concern the runtime adaptation of processes with active sessions, and the incorporation of recursive types and subtyping.
%in particular refinements for our notion of  interfaces, are discussed in 
%\S\,\ref{sec:int}.
%\S\,\ref{sec:recsub}.
%Some perspectives for enhanced updates are outlined .
Finally, \S\,\ref{sec:rw} discusses related work and \S\,\ref{sec:conc} collects some concluding remarks.

This paper is a revised version of the conference paper~\cite{DBLP:conf/sac/GiustoP13}, 
substantially 
extended 
with further examples and discussions.\done\todo[B2.]{We have reduced this paragraph, and moved the rest to the related work section.} %\footnote{Process $\adapt{l}{Q}{X}$ was written $l\{Q(\mathsf{X})\}$ in \cite{DBLP:conf/sac/GiustoP13}.}
%In particular, \S\,\ref{ss:examp}, which illustrates runtime adaptation patterns
%in an untyped setting, is new to this presentation, whereas 
% \S\,\ref{sec:exam}, \S\,\ref{sec:int}, and \S\,\ref{sec:rw} have been expanded significantly.
 See \S\,\ref{sec:rw} for further comparisons with respect to~\cite{DBLP:conf/sac/GiustoP13}. 
This presentation also contains the proofs of the main technical results; most of them are collected in the Appendix.



% 
 \section{A Process Language with Runtime Adaptation}\label{sec:syn}
We extend standard session-typed languages (see, e.g.,~\cite{DBLP:conf/esop/HondaVK98,DBLP:journals/entcs/YoshidaV07})
with \emph{located processes} and \emph{update actions}.
These two constructs, extracted from~\cite{BGPZFMOODS}, allow us to explicitly represent runtime adaptation 
within models of structured communications.
This section introduces the syntax and semantics of our process model, 
and illustrates some of the adaptation patterns expressible in it.\done\todo[B27.]{Fixed, dropping "we introduce", pls check.}
%\jp{As I explain below, we could (and probably should) avoid saying the following sentence.}
%As in~\cite{DBLP:conf/ppdp/GarraldaCD06}, 
%our process language 
%is instrumented with some elements which support the static analysis.
%In particular, we  
%annotate 
%located processes with an integer (representing established sessions).

\subsection{Syntax}
Our syntax builds upon the following  (disjoint)
base sets: 
\emph{names}, ranged over $a, b,  \ldots$;
\emph{locations}, ranged over $l, l', \ldots$;
\emph{labels}, ranged over $n, n', \ldots$;
\emph{constants} (integers, booleans, names), ranged over $c, c', \ldots$;\done\todo[C7.]{We have dropped "arithmetic" and have added other operations for constants.}
\emph{process variables}, ranged over $\mathsf{X}, \mathsf{X}', \ldots$.
%The sets of names and locations are assumed disjoint.
Then, \emph{processes}, ranged over $P, Q, R, \ldots$
and \emph{expressions}, ranged over $e, e', \ldots$
are given by the grammar in Table \ref{tab:syntax}.
%Our semantics uses 
We write $\widetilde{e}$ to denote 
a finite sequence of expressions $e_1, \ldots, e_n$; a similar convention applies for variables.
Notice that we also use 
\emph{(polarized) channels}, ranged over $\cha^{p}, \cha_1^{p}, \ldots$, where $p \in \{+,-\}$.
%and \emph{integers}, ranged over $j,h,m,\ldots$.
%Notice that we use identifier $k$ to denote  channels $\cha^{p}$ and names $x$.
\done\todo[B3.]{Here I have removed the reference to the semantics. We have clarified the channel/names notation in Table~\ref{tab:syntax}.}
In the following,  $j,h,m,\ldots$  range over 
%\emph{integers}.
$\mathbb{N}$.%\footnote{J: Cinzia, check this.}


%\emph{recursion variables}, ranged over $Y, Y', \ldots$;



\begin{table}[t]
$$
\begin{array}{lrlr}
a, b, c & ::=  &   x, y, z  & \text{variables}	\\
& \sepr &  u, v, w  & \text{names}	\\
 k & ::=  &   x, y, z  & \text{variables}	\\
& \sepr& \cha^{+}, \cha^{-} & \text{channels}	\\
P & ::=  &   \nopenr{a}{x}.P  & \text{session request}	\\
	& \sepr &   \nopena{a}{x}.P  & \text{session acceptance}	\\
	       & \sepr & \repopen{a}{x}.P  & \text{persistent session acceptance}	\\
	& \sepr &  \outC{k}{\widetilde{e}}.P & \text{data output}\\
  	&\sepr &    \inC{k}{\widetilde{x}}.P  & \text{data input}\\
	& \sepr &  \throw{k}{k'}.P & \text{channel output}\\
    &\sepr &   \catch{k}{x}.P  & \text{channel input}\\
	&\sepr&   \select{k}{n};P & \text{selection}\\
    	&\sepr&   \branch{k}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} & \text{branching}\\
%	&\sepr&  \component{l}{h}{\Delta}{P} ~~(h \geq 0)  & \text{adaptable process}\\
	&\sepr&  \scomponent{l}{P}   & \text{located process}\\
	&\sepr&  \adapt{l}{P}{\mathsf{X}}  %\sepr \migrate{l}{m}  \sepr  \destroy{l} 
	& \text{update process}\\
	    & \sepr &   \mathsf{X}& \text{process variable} \\
  	& \sepr &  \ifte{e}{P}{Q} & \text{conditional}\\
  	& \sepr &   P \para  P & \text{parallel composition}\\	 
		&\sepr&   \close{k}.P & \text{close session}	\\
			&\sepr&   \restr{k}{P}  & \text{channel hiding}	\\
			&\sepr&   \mathbf{0}  & \text{inaction} \\
%p	&::= &  + \sepr - &\text{channel polarities} \\
e	&::= &  c &\text{constants} \\
    & \sepr &   e_1 + e_2 \sepr e_1 - e_2  \sepr \mathtt{not}(e) \sepr  \ldots & \text{expressions}
\end{array} 
$$
\caption{Process syntax.} \label{tab:syntax}
\end{table}


We now comment on constructs in Table~\ref{tab:syntax}; in most cases, 
intuitions and conventions are as expected~\cite{DBLP:conf/esop/HondaVK98}.
Prefixes $\nopena{a}{x}$  and $\nopenr{a}{y}$ use name $a$ to establish a new session.
%\jp{We should hint why this is crucial to our approach.}
Once a session is established, structured behavior on channels is possible.
We sometimes refer to $\nopena{a}{x}.P$ as a \emph{service} 
%(for it may accept at most one session request on name $a$)
and to $\repopen{a}{x}.P $ as a \emph{persistent service}. %  (for it may accept zero or more requests on $a$).
In the same vein, we sometimes refer to $\nopenr{a}{x}.Q$ as a \emph{service request}.
Prefix $\close{k}$ is used to explicitly terminate session $k$. 
Having this prefix is crucial to our approach, for it allows us to keep track of the open sessions at any given time.
 The exchange of expressions is as usual; channel passing  
(delegation) is also supported.
Thus, our language supports %the usual dynamic reconfiguration 
transparent distribution of processing 
via channel passing
as well as the more expressive runtime adaptation via \emph{located} and \emph{update processes}, as we discuss below.
%For the sake of simplicity,
With the aim of highlighting the novel aspect of runtime adaptation, 
in this section
we consider infinite behavior in the form of replicated services; %, rather than as recursive definitions;
in \S\,\ref{sec:recsub}
%we do not foresee difficulties in extending our static analyses to a 
we show how to include recursion in the language.\done\todo[A6-A7.]{Here we should point to the new "extensions" section, explicitly mentioning co-inductive definitions.}
Also, we consider a restriction operator over channels only---restriction over names is not 
supported.
%included because we want full transparency.}
%\todo{dire anche qualcosa sul fatto che non c'e' restriction per i session name o per i locality name}


%\newpage
%\todo{nel type system abbiamo associato ad ogni locality l un interfaccia (un tipo) preciso, forse si puo' gia' dire qualcosa qui}

As hinted at in the Introduction, a \emph{located process} $\scomponent{l}{P}$ denotes a
process $P$  deployed at location~$l$.
Inside $l$, process $P$ can evolve on its own and interact with external processes.
In $\scomponent{l}{P}$, we use $l$ as a reference for a potential update action, which 
occurs by interaction with an \emph{update process} $\adapt{l}{Q }{\mathsf{X}}$---a built-in adaptation mechanism.
In $\adapt{l}{Q}{\mathsf{X}}$, 
we use $Q$ to denote a process  with zero or more occurrences of process variable $\mathsf{X}$.
%Intuitively,
As formalized by the operational semantics in~\S\,\ref{ss:opsem},
an \emph{update action} at $l$ corresponds to 
 the interaction of $\scomponent{l}{P}$ and $\adapt{l}{Q}{\mathsf{X}}$ which leads to process 
$Q\subst{P}{\mathsf{X}}$---the process $Q$ in which free occurrences of $\mathsf{X}$ are substituted with $P$.  
In the semantics, we shall consider \emph{annotated} located processes 
$\component{l}{h}{\Delta}{P}$, where $h$ %is a natural which 
stands for the number of active sessions in $P$.
This runtime annotation is used by the type discipline in \S\,\ref{s:types} to ensure that 
update actions do not disrupt the active session behavior deployed at a given location---this is the \emph{consistency} guarantee, formally addressed in \S\,\ref{ss:consist}.\done\todo[B4.]{In this paragraph (but also in the semantics) I have reversed the role of $P$ and $Q$, please check this is consistent.} %, we shall refer to this guarantee as \emph{consistency}.
%Furthermore, for each location $l$, the typing discipline assigns and maintains 
%a \emph{(service) interface} which succinctly describes the  services deployed at $l$.
%The intention is that any update actions on $l$ should at least maintain the service offer as described by its interface.

%$\component{l}{h}{\Delta}{Q}$. 
%$h$ stands for the number of active sessions in $Q$: 
%our operational semantics uses this information to ensure that locations enclosing active 
%sessions are not interrupted by update actions (consistency). 
%\jp{A better approach is to introduce syntax of located processes \emph{without} annotations, saying that $h$ is generated at runtime,
%and that our semantics is instrumented to use $h$.}


%\jp{The following is a bit different now:} In fact, as explained  below, 
%if the \emph{interfaces} of $Q$ and $P$ are 
%\emph{compatible} then 
%processes $\component{l}{h}{\INT_1}{Q}$ and $\adapt{l}{P}{X}$
%may interact so as to \emph{evolve} into $Q\subst{P}{\mathsf{X}}$.  
% Thus, 
% intuitively,
% process $\updated{l}{X}{\INT_1}{\INT_2}{Q}$ 
% behaves as a function which 
% expects a process with interface compatible with $\INT_1$ and 
% returns an adapted process with interface $\INT_2$.

Binding is as follows: 
%the channel 
variable $x$ is bound in processes 
$\nopenr{a}{x}.P$, ~$\repopen{a}{x}.P$, and $\nopena{a}{x}.P$; similarly, 
$\widetilde{x}$ is bound in $\inC{k}{\widetilde{x}}.P$ (variables $x_1, \ldots, x_n$ are all distinct). 
Also, process variable $\mathsf{X}$ is bound in the update process $\adapt{l}{P}{\mathsf{X}}$.
Based on these intuitions, given a process $P$, its sets of free/bound channels, variables, and process variables---noted 
$\mathsf{fc}(P)$, $\mathsf{fv}(P)$, $\mathsf{fpv}(P)$, $\mathsf{bc}(P)$, $\mathsf{bv}(P)$, and $\mathsf{bpv}(P)$, respectively---are defined as expected. 
%We define  $\mathsf{fu}(P) \triangleq \mathsf{fn}(P) \cup \mathsf{fc}(P)$.
%The treatment of recursion variables is also as customary. 
%As for process variables, we assume update processes bind process variables in it. 
%\jp{Free process variables??}
In all cases, we rely on expected notions of $\alpha$-conversion (noted $\equiv_\alpha$) and (capture-avoiding, simultaneous) substitution, noted
$\sub{\widetilde{c}}{\widetilde{x}}$ (for data), $\sub{\kappa^p}{{x}}$ (for channels), and $\sub{P}{\mathsf{X}}$ (for processes).
We work only with closed processes, and often omit the trailing $\nil$.

\subsection{Semantics}\label{ss:opsem}
%\todo{Spiegare bene quando compaiono i Kappa, i kappa compaiono a runtime}

The semantics of our process language is given by 
a \emph{reduction semantics},
denoted $P \pired P'$, the smallest relation on processes generated by the rules in Table~\ref{tab:semantics}.
As customary, it relies on  
an evaluation relation on expressions (noted $e \downarrow c$) and on
a structural congruence relation,  denoted $\equiv$, which we define next.

\begin{definition}[Structural Congruence]\label{d:strcong}
Structural congruence is  
the smallest congruence relation on processes that is generated by the following laws:%\footnote{Cinzia, notice that I have slightly changed the axioms, using $k$ instead of $\kappa$}
$$
\begin{array}{cc}
P \!\para \! Q \!\equiv\! Q \!\para \! P  &
(P \!\para \! Q) \!\para \! R \!\equiv\! P \!\para \! (Q \!\para \! R) \\
P \!\para \! \nil \!\equiv\! P  & 
P \!\equiv\! Q \text{ if } P \!\equiv\!_\alpha Q \\
\restr{\kappa}{\nil} \!\equiv\! \nil & \restr{\kappa}{\restr{\kappa'}{P}} \!\equiv\! \restr{\kappa'}{\restr{\kappa}{P}} \\
\restr{\kappa}{P} \!\para \! Q \!\equiv\! \restr{\kappa}{(P \!\para \! Q)} ~~\text{(if $\kappa \not\in \mathsf{fc}(Q)$)} &
\restr{\kappa}{\component{l}{h}{\Delta}{P}} \!\equiv\! \component{l}{h}{\Delta}{\restr{\kappa}{P}} 
\end{array}
$$
\end{definition}

\begin{table}[t]
{
$$
\begin{array}{ll}
 \rulename{r:Par} & \text{if } P \pired P' ~~\text{then} ~~ P \para Q \pired P' \para Q  \vspace{2mm}
\\
 \rulename{r:Res} &
\text{if } P \pired P' ~~\text{then} ~~ \restr{\cha}{P} \pired \restr{\cha}{P'} %\vspace{2mm} \\
\vspace{2.0mm} \\
 \rulename{r:Str} &
\text{if } P \equiv P',\, P' \pired Q', \,\text{and}\, Q' \equiv Q ~\text{then} ~ P \pired Q \vspace{2mm}
\\
 \rulename{r:Open} & 
E\big\{C\{\nopena{a}{x}.P\} \para  D\{\nopenr{a}{y}.Q\}\big\} \pired  \\
& 
\hfill E^{++}_{} \big\{\restr{\cha}{\big({C^{+}_{}\{P\sub{\cha^+}{x}\}  \para  D^{+}_{}\{Q\sub{\cha^-}{y}\} }\big)\big\} } \vspace{2.0mm} \\
\rulename{r:ROpen} & 
E\big\{C\{\repopen{a}{x}.P\}  \para  D\{\nopenr{a}{y}.Q\} \big\}  \pired  \\
& 
\hfill E^{++}_{}\big\{\restr{\cha}{\big({C^{+}_{}\{P\sub{\cha^+}{x}  \para \repopen{a}{x}.P \}  \para  D^{+}_{}\{Q\sub{\cha^-}{y}\} }\big)}\big\}  
 \vspace{2.0mm}\\
\rulename{r:Upd} & 
E\big\{C\{\component{l}{0}{}{P}\} \para  D\{\adapt{l}{Q}{X}\}\big\} 
\pired   %\\
%& \hfill 
E_{}\big\{C\{Q\sub{P}{\mathsf{X}}\}  \para  D\{\nil\}\big\} \vspace{2mm} \\
% \srulename{r:Move} & 
% E\big\{C\{\component{l}{h}{}{Q}\} \para  D\{\migrate{l}{m}\}\big\}~~ \pired   
% E_{}\big\{C\{\component{m}{h}{}{Q}\}  \para  D\{\nil\}\big\} \vspace{ 1.5mm} \\
% \srulename{r:Kill} & 
% E\big\{C\{\component{l}{0}{}{Q}\} \para  D\{\destroy{l}\}\big\}~~ 
% \pired   
% E_{}\big\{C\{\nil\}  \para  D\{\nil\}\big\} \vspace{ 1.5mm} \\
\rulename{r:I/O} &
E\big\{C\{\outC{\cha^{\,p}}{\widetilde{e}}.P\} \para  D\{\inC{\cha^{\,\overline{p}}}{\widetilde{x}}.Q\}\big\} 
\pired %\\
%& \hfill 
E\big\{C\{P\} \para  D\{Q\sub{\widetilde{c}\,}{\widetilde{x}}\}\big\} \quad (\widetilde{e} \downarrow \widetilde{c}) \vspace{2mm}
\\
\rulename{r:Pass} &
E\big\{C\{\throw{\cha^{\,p}}{\cha'^{\,q}}.P\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.Q\}\big\}\pired \hfill E\big\{C^{-}\{P\} \para  D^{+}\{Q\sub{\cha'^{\,q}}{x}\}\big\} %\\
%& \hfill E\big\{C^{-}\{P\} \para  D^{+}\{Q\sub{\cha'^{\,q}}{x}\}\big\} 
\vspace{2mm}
\\
\rulename{r:Sel} &
E\big\{C\{\branch{\cha^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m}\} \para  D\{\select{\cha^{\,\overline{p}}}{n_j};Q\}\big\} 
\pired \\
& 
\hfill E\big\{C\{P_j\}\para  D\{Q\}\big\}  \quad (1 \leq j \leq m)  \vspace{2mm}
\\
\rulename{r:Close} &
E\big\{C\{\close{\cha^{\,p}}.P\} \para  D\{\close{\cha^{\,\overline{p}}}.Q\}\big\} \pired %\\
%& \hfill 
E^{--}\big\{C^{-}\{P\} \para  D^{-}\{Q\}\big\} \vspace{ 2mm}
\\
\rulename{r:IfTr} &
C\{\ifte{e}{P}{Q}\} \pired C\{P\}  \quad (e \downarrow \mathtt{true})  \vspace{2mm}
\\
 \rulename{r:IfFa} &
C\{\ifte{e}{P}{Q}\} \pired C\{Q\}  \quad (e \downarrow \mathtt{false}) \vspace{2mm}
\end{array}
$$
}
\caption{Reduction semantics. } \label{tab:semantics}
\end{table}
\noindent In Table~\ref{tab:semantics}\done\todo[B5,B6.]{We need to properly answer this comment which concerns the rules.}, duality for polarities $p$ is as expected: $\overline{+} = -$ and $\overline{-} = +$. 
We write $\pired^{*}$ for the reflexive, transitive closure of $\pired$.
As processes can be arbitrarily nested inside %(transparent) 
locations, 
reduction rules use  \emph{contexts}, i.e., processes with a \emph{hole} $\bullet$.


\begin{definition}[Contexts]\label{d:context}
The set of \emph{contexts} is defined by the following syntax:
$$
C, D, E, \ldots ::=\bullet \sepr \component{l}{h}{\Delta}{C \para  P} %\sepr  \sepr \restr{\kappa}{C}  
$$
\end{definition}

%\jp{Why don't we have channel restriction in the syntax of contexts?}
%This way, g
Given a context $C$ 
%$C\{\bullet\}$ 
and a process $P$, 
we write $C\{P\}$ to denote the process obtained by filling in the occurrences of hole $\bullet$ in $C$ with $P$.
The intention is that $P$ may reduce inside $C$, thus reflecting the transparent containment realized by location nesting.\done\todo[B7.]{Add a sentence that is aligned with the reviewer's confusion and with the specific role that contexts play in our model. Perhaps we could call them "locating context" or something...}

We assume the expected extension of $\equiv$ to contexts; in particular, we tacitly use $\equiv$ to enlarge the scope of restricted channels in contexts as needed. As mentioned above, reduction relies on located processes with annotations $h$, which denote the number of active sessions at every location.
To ensure the coherence of such annotations along reduction, 
 we define operations over contexts
 which allow us to increase/de\-crease the annotation $h$ on every location contained in a context. 
 
 \begin{definition}[Operations on Contexts] \label{d:opcontx}
Given a context $C$ as in Def.~\ref{d:context}, a natural number $j$,
and an operator $* \in \{+,-\}$, %and $ \otimes \in \{\addelta, \midelta \}$, 
we define $C^{*j}$ as follows: 
$$ (\bullet)^{*j}_{}  = \bullet \qquad~~ (\component{l}{h}{\Delta}{C \para P})^{*j}_{} = \component{l}{{h*j}}{\Delta}{C^{*j}_{} \para P} %\quad~~ (C \para  P)^{*j}_{} = C^{*j}_{} \para  P 
$$
\end{definition}

This way, for instance, ${C}^{+1}$ 
denotes the context $C$ in which 
 the runtime annotations for all locations have been incremented by one.
We  write ${C}^{-}$, ${C}^{+}$, ${C}^{--}$, and ${C}^{++}$ to stand for ${C}^{-1}$, ~${C}^{+1}$, ${C}^{-2}$, and ${C}^{+2}$, respectively.


We now comment on reduction rules \rulename{r:Open}, \rulename{r:Upd}, \rulename{r:Pass}, and \rulename{r:Close} in Table~\ref{tab:semantics}; 
other rules are either standard or self-explanatory.

Rule \rulename{r:Open} formalizes session establishment. There are three distinguished contexts: while $C$ contains the %(linear) 
service offer and 
$D$ encloses the service request, context $E$ encloses both $C$ and $D$. %\done\todo[B9.]{We have said in Sect 2.1. that a linear service may execute at most once.}
By matching on name $a$ a session is established; 
following~\cite{DBLP:journals/acta/GayH05,DBLP:journals/entcs/YoshidaV07}, 
this is realized by endowing each partner with a fresh polarized channel (or end-point) $\kappa^p$.
As such, channels $\kappa^+$ and $\kappa^-$ are runtime entities. 
%with a fresh channel $c$; \jp{This is the point where we should explain runtime $\kappa$} at runtime, each process gets one end of the channel.
Because of session initiation, the number of active sessions 
should be increased across all enclosing contexts: relying on the operators given in Def.~\ref{d:opcontx}, we increment by one in contexts $C$ and $D$ and by two in context $E$, for it encloses both endpoints. 
This increment realizes a form of protection against careless update actions; observe that due to the  transparency of locations, any updates may take place independently from the actual nested structure.

The reasons for the increment just described should be clear from rule \rulename{r:Upd}, which formalizes the update/reconfiguration of a location $l$, 
enclosed in contexts $C$ and $E$.  
Notice how the update action can only occur if the number of open (active) sessions in $l$ is 0.
By forcing updates to occur only when any (located) session behavior has completed (cf. rule \rulename{r:Close}), reduction ensures that 
active sessions are not inadvertently disrupted. %update actions which may interrupt session communications.
When enabled, an update action  is  realized by 
  substituting, within location $l$, all free occurrences of $\mathsf{X}$ in $Q$ with $P$ (the current behavior at $l$). Hence,  it is the adaptation routine which ``moves''   to realize reconfiguration. This is a form of \emph{objective update}, as the located process does not 
contain information on future update actions: it reduces autonomously until it is adapted by an update process in its environment. 

Rule \rulename{r:Pass} is the standard rule for delegation; in our setting, endpoint mobility is reflected by appropriate decrements/increments in the contexts enclosing the session sender/receiver. 
Rule~\rulename{r:Close} formalizes the synchronized session closure. In analogy with rule \rulename{r:Open}, session closure 
should decrease the active session annotation in all enclosing contexts.
%\jp{We no longer need to refer to interfaces here, only to the fact that runtime annotation $h$ is used to avoid inconsistent updates}
%Let us write $\intf{P}$ for the \emph{interface} of process $P$ (cf. Sect.~\ref{s:types}). 

\subsection{Examples of Runtime Adaptation}\label{ss:examp}

%\begin{example}
%In order to illustrate the syntax and semantics of our framework, 
We now present 
some patterns of runtime adaptation that can be expressed in our process framework.
Recall that $l_1, l_2, \ldots$ denote identifiers for locations.
We discuss different reductions, resulting from the interaction between a located process and a corresponding adaptable process.
These reductions are \emph{enabled}; for the sake of readability, however, we elide the runtime annotation 
associated to the locations ($h = 0$ in all cases).


%We give here some examples on how adaptable processes can be used:
 \begin{description}
 \item[Relocation.] One of the simplest reconfiguration actions that 
 can be represented in our model is the relocation of an arbitrary behavior %at a location 
 to a completely different
 computation site. 
 The following reduction illustrates how a synchronization on location $l_1$ leads to 
 a relocation from $l_1$ to $l_2$:
% Similarly, one can think of moving the content of a locality $a$ into a fresh locality $b$:
$$\bigcomponent{l_1}{}{}{\,\compo{l_4}{}{Q}\,} \para \adapt{l_1}{\compo{l_2}{}{ \mathsf{X} }}{ \mathsf{X} } \pired \bigcomponent{l_2}{}{}{\,\compo{l_4}{}{Q}\,} \para \nil $$
It is worth observing how a relocation does not alter the behavior at $l_1$.
In particular, relocations are harmless to open sessions in $Q$, if any.
 
\item[Deep Update.] 
Because our locations are transparent, an update action may have influence on located processes not necessarily at top-level
in the nested process structure. 
The reduction below illustrates how the influence of an update process on name $l_3$ can cross locations $l_1$ and $l_2$ in order
to realize an adaptation routine, represented by process $S'$:
%We start with an example that underlines the transparency of adaptable processes, here we are going to substitute the adaptable process located at $c$ with a new adaptable process $S'$ located inside $d$. Notice that $c$ occurs inside $b$ that is on its turn inside $a$. Thus:
$$\bigcomponent{l_1}{}{}{Q \para \bigcomponent{l_2}{}{}{R \para \compo{l_3}{}{S_{1}} }\,} \para 
\adapt{l_3}{\compo{l_4}{}{S'}}{ \mathsf{X} } 
\pired 
\bigcomponent{l_1}{}{}{Q \para \compo{l_2}{}{R \para \compo{l_4}{}{S_{2}}\, }\, } \para \nil $$
where $S_2 = S'\sub{S_1}{\mathsf{X}}$.
That is, by virtue of the update action on $l_3$, its current behavior  (denoted $S_1$) is suspended 
and possibly used in the new behavior $S'$, which is now located at~$l_4$.

 \item[Upgrade.] Interestingly, update actions do not need to preserve the current behavior at a given location. 
 In fact, if the adaptation routine embodied by the updated process does not contain a process variable, 
 then the current behavior at the location will be discarded.
 This feature is illustrated by the following reduction, in which we assume that $\mathsf{X} \notin \mathsf{fv}(Q)$:
 % Next, we show how to destroy locality $a$ and its content. In this case we require $\mathsf{X} \notin \mathsf{fv}(Q)$, this way $Q$ is a closed process and $Q\sub{P}{\mathsf{X}}= Q$ thus obtaining:
$$ \compo{l_1}{}{P} \para \adapt{l_1}{Q}{\mathsf{X}} \pired Q \para \nil $$
Observe that the location on which the update action takes place does not need to be preserved either:
had we wanted to only replace the behavior at $l_1$, then it would have sufficed\done\todo[B29.]{Fixed, pls check.} to enclose 
the runtime adaptation code $Q$ within a located process named $l_1$, i.e.,
%recreate the locality $a$ in the update construct:  
$\adapt{l_1}{\compo{l_1}{}{Q}}{\mathsf{X}}$. 


\item[Conditional Backup.]   The current behavior of a location may be used more than once by an
adaptation routine.
Consider process $B_e$ below:
$$
B_e = \compo{l_1}{}{Q} \para \bigcomponent{l_5}{}{}{\,
\ifte{e}{\adapt{l_1}{\compo{l_2}{}{\mathsf{X}}}{\mathsf{X}}}{\adapt{l_1}{\compo{l_1}{}{\mathsf{X}}{} \para \compo{l_3}{}{\mathsf{X}}}{\mathsf{X}}}\,}
$$
Depending on the boolean expression $e$ reduces to, 
$B_e$ may either (i) simply relocate the behavior at $l_1$, 
or (ii) define a ``backup copy''  of $Q$ at  $l_3$: %. More precisely:
\begin{eqnarray*}
B_e & \pired^* & \compo{l_2}{}{Q} \para \compo{l_5}{}{\nil} \quad \qquad \qquad\text{if $e \downarrow \mathtt{true}$} \\
B_e & \pired^* & \compo{l_1}{}{Q} \para \compo{l_3}{}{Q} \para \compo{l_5}{}{\nil} \qquad\text{if $e \downarrow \mathtt{false}$}
\end{eqnarray*}
\end{description}

\noindent
The previous examples are useful to illustrate the expressiveness of adaptable processes for representing 
rich  adaptation mechanisms. As our process model includes both communication and update actions,
we require mechanisms for harmonizing %both kinds of actions, 
them, \done\todo[B30.]{Fixed, pls check.}
avoiding undesirable disruptions of communication behavior by updates.
In the next section, we define a static analysis technique that enables update actions when 
the given location does not enclose open sessions.



% 
 \section{The Type System}\label{s:types}
Our type system builds upon the one in~\cite{DBLP:journals/entcs/YoshidaV07},
extending it so as to account for disciplined runtime adaptation.
%\cite{DBLP:conf/ppdp/GarraldaCD06}.
%As mentioned in the Introduction, a 
A
main criteria in the design of our type discipline is \emph{conservativity}:
we would like to enforce both structured communication and disciplined adaptation by preserving standard models of session types as much as possible. \done\todo[B31.]{Fixed, pls check.} 

\subsection{Type Syntax}
We now define our type syntax, which is rather standard.
%Our type syntax is as follows: %defined next, contains the usual session types constructs: %---we exclude recursive types.

%As such, the type syntax is divided into three categories: \emph{basic types}, which  handle expressions; 
%\emph{pre-session types} describing a channel's ability for sending/receiving messages and offering/selecting be\-hav\-iors; 
%\emph{session types} representing well-formed session-typed be\-hav\-ior. %; and
%\emph{channel types}, which can be a session type or a \emph{used session}~$\bot$. %this will be made clear later on).

%We extend the judgments of~\cite{DBLP:conf/ppdp/GarraldaCD06} with an \emph{interface} $\INT$---the collection of all session types declared in a given process. 
%
%Formally, we have:

%\end{document}
 
\begin{definition}[Types]\label{d:types}
The syntax of 
 \emph{basic types} (ranged over $\capab, \sigma,   \ldots$) %, \emph{pre-session types} ($\zeta$), 
 and
 %(qualified) 
 \emph{session types} (ranged over $\ST, \beta, \ldots$)
% and \emph{channel types} ($\omega$) 
is given in Table~\ref{tab:types}.
\end{definition}

\begin{table}[t!]
\textsc{Types}
$$
\begin{array}{lclr}
\capab, \sigma & ::= & \mathsf{int} \sepr \mathsf{bool} \sepr \dots ~~~& \text{basic types}\\

\alpha, \beta &::=  &  !(\widetilde{\capab}).\alpha \sepr ?(\widetilde{\capab}).\alpha & \text{send, receive} \\ 
		& \sepr &  !(\beta).\alpha \sepr ?(\beta).\alpha & \text{throw, catch} \\ 
		& \sepr &  \&\{n_1:\alpha_1, \dots,  n_m:\ST_m \}  \quad &  \text{branch} \\
		& \sepr &  \oplus\{n_1:\alpha_1, \dots , n_m:\ST_m \}  &  \text{select} \vspace{0.5mm} \\
		& \sepr &  \epsilon \!\!\!\!\!\!& \text{closed session}
\end{array}
$$
\textsc{Environments}
$$
\begin{array}{lclr}
		\qua & ::= &  \qual \sepr \quau  & \text{type qualifiers} \vspace{0.5mm} \\
%\INT &::= &  \emptyset \sepr \INT, \langle a: \ST, h \rangle & \text{interface} \\
\ActS & ::= &  \emptyset \sepr \ActS , k:\ST \sepr \ActS ,  [k:\ST]  & \text{typing with active sessions}\\
\Gamma &::= &  \emptyset \sepr \Gamma, e:\capab \sepr \Gamma, a:\langle \ST_\qua , \overline{\ST}_\qua \rangle \quad& \text{first-order environment}\\
\Theta &::= &  \emptyset \sepr  \Theta,\mathsf{X}:\INT \sepr \Theta,l:\INT     \quad& \text{higher-order environment}
\end{array}
$$  
\caption{Types and Typing Environments. Interfaces $\INT$ are formally introduced in Definition~\ref{d:interf}.}\label{tab:types}
\end{table}



% We use $t, t', \ldots$ to range over \emph{type variables}; also, we 
% require recursive types to be \emph{contractive}, i.e., not 
% containing a subexpression of the form $\mu t.\mu t_1.\cdots.\mu t_n.t$.
% Binder $\mu$ gives rises to standard notions of free/bound type variables; 
% $\mathsf{ftv}(\zeta)$ denotes the free type variables in $\zeta$.
% We consider session types modulo folding/unfolding of recursive types.
%\todo{contractive types?}
We recall the intuitive meaning of session types. 
We write $\til{\tau}$ to denote a sequence of base types $\tau_1, \ldots, \tau_n$.
Type $?(\til{\capab}).\ST$ (resp. $?(\beta).\ST$) abstracts the behavior of a channel 
which receives values of types $\til{\capab}$ (resp. a channel of type $\beta$) 
and continues as $\ST$ afterwards.
Complementarily, type $!(\til{\capab}).\ST$ (resp. $!(\beta).\ST$) represents the behavior
of a channel which sends values (resp. a channel)  and that continues as $\ST$ afterwards.
Type $\&\{n_1:\alpha_1, \dots,  n_m:\ST_m \}$ describes a branching behavior, or external choice, along a channel:
it offers $m$ behaviors, and if the $j$-th alternative is selected then it behaves as described by type $\ST_j$ ($1 \leq j \leq m$).
In turn, type $\oplus\{n_1:\alpha_1, \dots , n_m:\ST_m \}$ describes the behavior of a channel which 
may select a single behavior among  $\alpha_1, \ldots, \alpha_m$. This is an internal choice, which continues as $\ST_j$ afterwards.
Finally, type $\epsilon$ represents a channel with no communication behavior. 
We now introduce the central notion of  \emph{duality} for (session) types.


\begin{definition}[Duality]\label{d:dual}
Given a session type $\ST$, 
its \emph{dual}
(noted $\overline{\ST}$) is inductively defined in Table~\ref{tab:dual}.
\begin{table}[t]
$$
\begin{array}{rcl}
 \overline{\epsilon} & =  & \epsilon\\
 \overline{!(\til{\capab}).\ST} & =  & ?(\til{\capab}).\overline{\ST} \\
 \overline{?(\til{\capab}).\ST} & =  & !(\til{\capab}).\overline{\ST} \\
 \overline{!(\beta).\ST} & =  & ?(\beta).\overline{\ST} \\
 \overline{?(\beta).\ST} & =  & !(\beta).\overline{\ST} \\
% \overline{t} &\!\!=\! & t \\
 %\overline{\mu t.\ST} &\!\!=\! & \mu t.\overline{\ST}\\
 \overline{\&\{n_1:\ST_1 , \ldots , n_m:\ST_m \}} &\!\!=\! & \oplus\{n_1:\overline{\ST_1} , \ldots , n_m:\overline{\ST_m} \}\\
 \overline{ \oplus\{n_1:\ST_1 , \ldots , n_m:\ST_m \}} &\!\!=\!& \&\{n_1:\overline{\ST_1} , \ldots , n_m:\overline{\ST_m} \}
\end{array}
$$ %\vspace{-4mm}
\caption{Dual of session types}\label{tab:dual}
\end{table}
\end{definition}

%Before introducing our notion of typing environment
\done\todo[B32.]{Fixed, pls check.}
Our typing judgments generalize usual notions with an  \emph{interface}~$\INT$ (see Def.~\ref{d:interf}). 
Based on the syntactic occurrences of prefixes $\nopenr{a}{x}$, $\nopena{a}{x}$, and $\repopen{a}{x}$,
the interface of a process describes the (possibly persistent) services appearing in it.
Thus, intuitively, the interface of a process gives an ``upper bound'' on the services that a process may execute.
Formally, we have:
%We now formally define the concept of interface, motivated above.
%Recall that we use $j,h,\ldots$ to range over 
%$\mathbb{N}_0$.
%integers.
%\done\todo[B10.]{Added a note concerning $h$, missing some other two issues.}

%\begin{definition}[Interfaces OLD]\label{d:interfold}
%An \emph{interface} $\INT$ is a set of pairs  $\langle a: \ST, h\rangle$ where 
%$a$ is name, $\ST$ is a session type, and either $h> 0$ or $h = \infty$.
%The extension of an interface $\INT$ with a pair $\langle a: \ST, h\rangle$, written $\INT \addelta \inter{a}{\alpha}{h}$,
%is defined as follows:
%$$
%\INT \addelta \inter{a}{\alpha}{h} \triangleq
%\begin{cases}
%\INT' \cup \{\inter{a}{\ST}{h + j} \} & \text{if } \exists\INT'. \,  \INT = \INT' \cup \{\inter{a}{\ST}{j} \}	\\
%\INT \cup \{\inter{a}{\ST}{h}\} & \text{otherwise} 
%\end{cases}
%$$
%Given $\INT$, we write $\INT_\quau$ 
%and $\INT_\qual$
%to denote sets $\{ \inter{a}{\ST}{h} \,|\, \inter{a}{\ST}{h} \in \INT \land h = \infty\}$ and
%$\INT - \INT_\quau$, respectively. \\
%Moreover, we write $\INT \unres$ 
%to denote the set $\{ \inter{a}{\alpha}{\infty} \mid   \inter{a}{\alpha}{h} \in \INT_\qual \} \cup \INT_\quau$.
%%Finally we define the  function $$\unres(\INT) \triangleq \{ \inter{a}{\alpha}{\infty} \mid   \inter{a}{\alpha}{h} \in \INT \}$$
%\end{definition}


\begin{definition}[Interfaces]\label{d:interf}
We define an \emph{interface} as the multiset whose underlying set of elements 
$\mathrm{Int}$ contains 
assignments from names to session types which are qualified (cf. Table~\ref{tab:types}).
More precisely: $$\mathrm{Int} = \{ \qua\,a{:}\ST ~|~ \qua \in \{\qual, \quau\}, 
\text{$a$ is a name, and $\ST$ is a session type}\}$$
We use $\INT, \INT', \ldots$ to range over interfaces.
We sometimes write $\#_\INT(a) = h$ to mean that element $a$ occurs $h$ times in $\INT$.
\end{definition}

%
%OLD TEXT: We recall that $\infty + 1 = \infty$.
%Intuitively, interfaces capture the services declared in a process\todo[C8.]{Clarify intuitions for interfaces?} (i.e., an assignment from names to session types)
%together with
%the number of times such a service is declared ($j>0$ if a type is linear; $\infty$ otherwise).
%In $\INT$, services are recorded at most once; several occurrences of the same linear service are captured
%by the second component of the pair.   
%We sometimes write $\INT \addelta a:\ST_\qual$ 
%and  $\INT \addelta a:\ST_\quau$
%to stand 
%for $\INT \addelta\{\inter{a}{\ST}{1} \}$ and 
%$\INT \addelta \{\inter{a}{\ST}{\infty} \}$, respectively.
%The extension of $\addelta$ from single pairs $\inter{a}{\ST}{h}$ 
%to interfaces, denoted $\INT_1 \addelta \INT_2$, is as expected. 


%NEW TEXT: 
%Intuitively, interfaces capture the services declared in a process, including their possibly persistent nature.
Observe how several occurrences of the same service declaration are captured by the multiset nature of interfaces.
The union of two interfaces $\INT_1$ and $\INT_2$ is essentially the union of their underlying multisets.
We sometimes write $\INT \addelta a:\ST_\qual$ 
and  $\INT \addelta a:\ST_\quau$
to stand 
for $\INT \addelta\{\qual\,a{:}\ST\}$ and 
$\INT \addelta \{\quau\,a{:}\ST\}$, respectively.

\begin{newnotation}[Interfaces]\label{n:interf}
We write $\INT_\qual$ (resp. $\INT_\quau$) to denote the subset of $\INT$ involving
only assignments qualified with $\qual$ (resp. $\quau$). 
Moreover, we write $\INT \unres$ to denote the ``persistent promotion'' of $\INT$. Formally, 
$\INT \unres = \INT \setminus \INT_\qual \addelta \{\quau\,a{:}\ST \mid   \qual\,a{:}\ST \in \INT_\qual \}$.
%Furthermore, we write $\INT  \intpr \INT'$  to denote that interface $\INT$ is included in $\INT'$.
\end{newnotation}

It is useful to relate different interfaces. % which only differ in the linear services they contain.
This is the intention of the relation $\intpr$ over interfaces, defined next.
%
%\begin{definition}[OLD Interface Ordering] \label{d:intpre}Given interfaces $\INT$ and $\INT'$, we write 
%$\INT  \intpr \INT'$ iff 
%\begin{enumerate}[1.]
%\item $\INT_\qual \subseteq \INT'_\qual$, where $\subseteq$ is the usual ordering on multisets; 
%\item $\forall (\quau\,a{:}\ST) \in \INT_\quau $  then 
%$ (\quau \, a{:}\ST) \in \INT'_\quau $.
%\done\todo[B11.]{We need to understand this comment.}
%\end{enumerate}
%\end{definition}
%
\begin{definition}[Interface Ordering] \label{d:intpre}Given interfaces $\INT$ and $\INT'$, we write 
$\INT  \intpr \INT'$ iff 
\begin{enumerate}[1.]
\item 
One of the following holds:
\begin{enumerate}[(a)]
\item $\INT_\qual \subseteq \INT'_\qual$, where $\subseteq$ is the usual ordering on multisets, or 
\item $\forall (\qual\,a{:}\ST) \in \INT_\qual \setminus \INT_\qual'$ then  $(\quau\,a{:}\ST) \in \INT'_\quau$
\end{enumerate}
\item $\forall (\quau\,a{:}\ST) \in \INT_\quau $  then $ (\quau \, a{:}\ST) \in \INT'_\quau $.
\end{enumerate}
Interface equality is defined as: $\INT_1 = \INT_2$ iff  $\INT_1 \intpr \INT_2$ and $\INT_2 \intpr \INT_1$
\end{definition}

In the light of the previous definitions, we may state:

\begin{lemma}
Relation \intpr is a preorder.
\end{lemma}
%
%As we will see, our typing system will be parametric on the definition of \intpr.
%Alternative definitions for this relation are discussed in Sect.~\ref{sec:int}.
\done\todo[B12.]{We need to understand this comment.}

\subsection{Environments, Judgments and Typing Rules}
The typing environments we rely on are defined in the lower part of Table~\ref{tab:types}.
In addition to interfaces $\INT$, we consider typings $\ActS$ and environments $\Gamma$ and $\Theta$.

%In session type disciplines, 
Typing $\ActS$ is commonly used to collect
assignments from channels to session types; as such, it describes
currently active sessions. 
In our discipline, 
%Unlike usual disciplines, however, 
in $\ActS$ we also include \emph{bracketed assignments}, denoted $[\kappa^p:\ST]$,
which represent active but restricted sessions. 
As we discuss below, bracketed assignments arise in the typing of %channel 
restriction, 
and are key to keep a precise count of the active sessions in a given located process. \done\todo[A8.]{Slightly rephrase to emphasize on the need of correctness of counting.} 
We write $dom(\ActS)$ to denote the set $\{ k^p \mid k^p:\ST \in \ActS \lor [k^p:\ST] \in \ActS\}$.
We write $\ActS , k:\ST $ and $\ActS , [k:\ST] $ where $k \not\in dom(\ActS)$. % (and similarly for the other environments).


$\Gamma$ is a first-order environment which maps expressions to basic types
and names to pairs of \emph{qualified} session types.
In  the interface, a session type is qualified with 
`$\quau$' if it is associated to a persistent service; otherwise, it is qualified with 
`$\qual$'.
%While $\qual$ is used for those session types %to be used %just once, 
%associated to linear services, we use 
%$\quau$ to qualify  session types %intended to feature a persistent behavior.
%associated to persistent services.\todo[B13.]{I have used the linear/persistent terminology introduced before. Please check.}

The higher-order environment $\Theta$ 
collects assignments of process variables and locations to interfaces. 
While the former kind of assignments is relevant to update processes, the latter concern located processes.
As we explain next, by relying on the combination of these two pieces of information the type system ensures that
runtime adaptation actions preserve the behavioral interfaces of a process.
%\jp{The following is a bit strange for locations are also in $\T$; I would write $vdom(\T)$ if you only care about variables.} \todo{
We write $vdom(\Theta)= \{ \mathsf{X} \mid \mathsf{X}:\INT \in \Theta \}$ to denote the variables in the domain of $\Theta$.
%}
Given these environments, a \emph{type judgment} is  of form
$$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} $$ 
meaning that, under environments $\Gamma$ and $\Theta$, 
process $P$ has active sessions declared in $\ActS$ and interface 
$\INT$.\done\todo[B14.]{I changed the notation for judgments, please check consistency.} We then have:

\begin{definition}%[Well-typed process]
A process is well-typed if it can be typed using the rules in Tables~\ref{tab:ts} and~\ref{tab:session}.


\begin{table}[th!]
$$
\begin{array}{c}
% \mathrm{\textsc{Comp}}~~~\component{a}{P} \arro{~\component{a}{P}~}  \star
\inferrule*[left=\rulename{t:Exp}]{ }{\Gamma \vdash e:\capab}{}\done\todo[B34.]{We have single typing rule per line, please check.} 
\vspace{2mm} \\
\inferrule*[left=\rulename{t:NVar}]{ }{\Gamma, x:\capab \vdash x:\capab} 
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Nil}]{ }{\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:LocEnv}]{ }{\Theta, l:\INT \vdash l:\INT} 
\vspace{2mm} \\
\inferrule*[left=\rulename{t:PVar}]{ }{\Gamma; \Theta,\mathsf{X}:\INT \vdash \mathsf{X}:\type{\emptyset}{\INT}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Accept}]{\Gamma \vdash a: \langle \ST_\qual , \overline{\ST}_\qual  \rangle \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\ST}{\,\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P}{ \type{\ActS}{\,\INT \addelta a: \ST_\qual}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:RepAccept}]
 {\Gamma \vdash a: \langle \ST_\quau , \overline{\ST}_\qual  \rangle \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{x:\ST}{\,\INT}} 
}{\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P}{ \type{\emptyset}{\INT\unres \addelta \, a: \ST_\quau}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Request}]
 {
\Gamma \vdash a: \langle \ST_\qua , \overline{\ST}_\qual \rangle \qquad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\overline{\ST }}{\,\INT}} 
}{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{x}.P}{ \type{\ActS}{\,\INT \addelta a: \overline{\ST}_\qual }}} 
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Clo}]
 {\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}} \qquad k\notin \dom{\ActS} }{\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS, k:\epsilon}{ \INT}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Loc} ]
 {
       \Theta \vdash l:\INT \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } } \qquad  h = | \ActS |  \qquad \INT' \intpr \INT
 }{\judgebis{\env{\Gamma}{\Theta}}{\component{l}{h}{\INT}{P} }{ \type{\ActS}{\INT' }}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Adapt} ] 
{\Theta \vdash l:\INT  \qquad  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT}}}{P}{\type{\emptyset}{ \INT' }}}{\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{X}}{\type{\emptyset}{ \emptyset}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:CRes}]
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Par}]
 {
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \qquad
 \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
 }{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT_1 \addelta \INT_2}}}
 \end{array}
 $$
\caption{Well-typed processes (I)} \label{tab:ts}
\end{table}
\end{definition}



\begin{table}[th!]
$$
\begin{array}{c}
\inferrule*[left=\rulename{t:Thr}] 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT}{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\throw{k}{k'}.P}{\type{\ActS, k:!(\ST).\STT, k':\ST}{ \INT}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Cat}]
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT, x:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\catch{k}{x}.P }{\type{\ActS, k:?(\ST).\STT}{ \INT}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:In}]
{\judgebis{\env{\Gamma, \til{x}:\til{\capab}}{\Theta}}{P}{\type{\ActS, k:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\inC{k}{\til{x}}.P }{\type{\ActS, k:?(\til{\capab}).\ST}{ \INT}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Out}]
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST}{ \INT}} \quad \Gamma \vdash \til{e}:\til{\capab}}{\judgebis{\env{\Gamma}{\Theta}}{\outC{k}{\til{e}}.P}{\type{\ActS, k:!(\til{\capab}).\ST}{ \INT}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Weak}] 
{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{ \INT}  } \qquad \cha^+, \cha^- \notin dom(\ActS)}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS}{ \INT }}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:If}]
 {
 \Gamma \vdash e:\mathsf{bool} \qquad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} \qquad
\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}
 }{\judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{\type{\ActS}{\INT}}} 
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Bra}] 
{
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS, k:\ST_1}{ \INT_1}} 
\quad 
\cdots
\quad
\judgebis{\env{\Gamma}{\Theta}}{P_m}{\type{\ActS, k:\ST_m}{ \INT_m}} \quad \INT = \INT_1 \uplus ...\uplus \INT_m
 }{\judgebis{\env{\Gamma}{\Theta}}{\branch{k}{n_1{:}P_1 \alte \cdots \alte  n_m{:}P_m}}{\type{ \ActS, k:\&\{n_1{:}\ST_1, \ldots, n_m{:}\ST_m \}}{\INT}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Sel}]
{
\judgebis{ \env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST_i}{ \INT}} \qquad 1 \leq i \leq m 
}{\judgebis{\env{\Gamma}{\Theta}}{\select{k}{n_i};P}{\type{\ActS, k:\oplus\{n_1:\ST_1, \ldots,  n_m:\ST_m \}}{\INT}}}
\end{array}
$$% \vspace{-4mm}
\caption{Well-typed processes (II)}\label{tab:session}
\end{table}




We comment on some %non standard 
rules in Table~\ref{tab:ts}.
Given a process which implements session type $\ST$  on channel $x$, 
rule \rulename{t:Accept} types a service on name~$a$. 
Observe how $x$ is removed from $\ActS$ whereas
 $\INT$ is appropriately extended with $a : \ST_\qual$. Rule \rulename{t:RepAccept} is the analogous of \rulename{t:Accept} for persistent services.
In that rule, observe how the linear services in  $\INT$ are ``promoted'' to persistent services via $\INT\unres$ (cf. Not.~\ref{n:interf}).
%\todo{
Non persistent services that appear in the context of a persistent service $a$ are meant to be executed %exactly 
at most
once for each instance of $a$. 
In fact, after promotion the declaration in $\Gamma$ for a non persistent service $b:\langle \ST_{\qual}, \overline{\ST}_{\qual} \rangle$ remains unchanged, but its entry in $\INT$ should be 
%$\inter{b}{\ST}{\infty}$, 
$\quau\,b{:}\ST$,
as we could now observe an unbounded number of executions of (non persistent) service $b$.
%}
%\jp{Cinzia, please check I didn't modified the intended meaning of your text.}
Given these typing rules, rule \rulename{t:Request} should be self-explanatory.

Rule~\rulename{t:CRes} types channel restriction. 
The main difference wrt usual typing rules for channel restriction (cf.~\cite{DBLP:journals/entcs/YoshidaV07}) is that 
restricted end-points are not removed from $\ActS$ but kept in bracketed form, as motivated earlier. 
Using typing $\ActS$,
we can have an exact count of open, possibly restricted, sessions in a process.
Rule~\rulename{t:Close} types the explicit session closure construct, extending 
$\ActS$ with a fresh channel which is assigned to an empty session type. 
This may be useful to understand why our typing rule for the inactive process (rule \rulename{t:Nil})
requires an empty typing $\Delta$.

%\jp{Far notare la nostra regola Rule \rulename{t:Nil} inizia da un $\Delta$ vuoto...}
Rule~\rulename{t:Loc} performs two checks to type located processes. First, the runtime annotation 
$h$ is computed by counting the assignments (standard and bracketed) declared in $\ActS$ (see~\ref{ap:count}). \done\todo[A9.]{This is extremely silly, but it is better to add the formal definition of $|\Delta|$}
Second, the rule checks that the interface of the located process is less  or equal (in the sense of $\intpr$, cf. Not.~\ref{n:interf}) than the
declared interface of the given location. 
Informally, this ensures that the process behavior does not ``exceed'' the expected behavior within the location.
It is worth observing how a typed located processes has the exact same typing and interface of its contained process:
this is how transparency of locations arises in typing.
Finally, rule \rulename{t:Adapt} types update processes. Observe how the interface associated to the process variable of the given 
 adaptation routine should match with the declared interfaces for the given location. 
However, for simplicity we establish no condition on the relation between $\INT$ (the expected interface) 
and $\INT'$ (the interface of the adaptation routine $P(\mathsf{X})$)
%---Sect.~\ref{sec:int} 
---in \S\,\ref{sec:recsub} we discuss an alternative, more stringent, formulation.
%\jp{Should we say something about $\INT'$?, yes but not here}
%This way, the rule guarantees that the process resulting from an update action has the declared interfaces. 

Having introduced our typing system, the following section defines and states its main properties.

%Rule \rulename{t:Par} puts processes in parallel. 
%Rules \rulename{t:PVar}  handle process  variables. 
%Rule \rulename{t:Weak} handles all those processes in which $\restr{c}{P} \equiv P$ holds, and 
%\rulename{t:CRes} types channel restriction. 
%While rules \rulename{t:Cat} and \rulename{t:Thr} handle delegation,
%rules \rulename{t:In}, \rulename{t:Out},  \rulename{t:If}, 
%\rulename{t:Bra},  and \rulename{t:Sel} are standard.




%\todo{Properties of the type system
%\begin{enumerate}
%\item Weakening and strengthening lemmas
%\item Substitution lemma
%\item Subject congruence 
%\item Subject reduction, for balanced environments
%\item Type safety (with appropriate definitions of error)
%\end{enumerate}
%}

% 
 \section{Session Safety and Consistency by Typing}\label{sec:res}
\newcommand{\jug}{\ensuremath{\mathcal{S}}}

We now proceed to investigate\done\todo[B35.]{Fixed, pls check.} \emph{safety} and \emph{consistency}, the main properties of our typing system.
While safety (discussed in \S\,\ref{ss:safety}) corresponds to the expected guarantee of adherence to prescribed session types and absence of runtime errors, 
consistency (discussed in \S\,\ref{ss:consist})  formalizes a correct interplay between communication actions and update actions.
Defining both properties requires the following notions of \emph{$\kappa$-processes}, \emph{$\kappa$-redexes}, 
and \emph{error process}.
These are classic ingredients in session types presentations (see, e.g., \cite{DBLP:conf/esop/HondaVK98,DBLP:journals/entcs/YoshidaV07});
our notions generalize usual definitions 
to the case in which processes which may interact even if contained in arbitrarily nested transparent locations (formalized by the contexts of 
Def.~\ref{d:context}).

\begin{definition}[$\kappa$-processes, $\kappa$-redexes, errors]\label{d:kred}
A process $P$ is a \emph{$\kappa$-process} if it is a prefixed process with subject $\kappa$, i.e., 
$P$ is one of the following:
$$
%\begin{array}{llcllcrl}
%  &  \inC{\kappa^{\,p}}{\til{x}}.P' & &  & \outC{\kappa^{\,p}}{v}.P' & &    &  \close{\kappa^{\,p}}.P'  \\
%  &   \catch{\kappa^{\,p}}{x}.P' & &  &    \throw{\kappa^{\,p}}{d^{\,q}}.P' \\
%  &   \branch{\kappa^{\,p}}{n_1{:}P_1 \parallel \ldots \parallel n_m{:}P_m} ~~ & &  &   \select{\kappa^{\,p}}{n}.P' 
%\end{array}
\begin{array}{ll}
    \inC{\kappa^{\,p}}{\til{x}}.P' & \outC{\kappa^{\,p}}{v}.P'    \\
  \catch{\kappa^{\,p}}{x}.P' &  \throw{\kappa^{\,p}}{k^{\,q}}.P' \\
   \branch{\kappa^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m}  &   \select{\kappa^{\,p}}{n}.P' \\
    \close{\kappa^{\,p}}.P' & 
\end{array}
$$
Process $P$ is a \emph{$\kappa$-redex} if 
it contains the composition of exactly two $\kappa$-processes with opposing polarities, i.e., 
for some contexts $C$, $D$ and $E$\done\todo[B36.]{Fixed, pls check}, and processes $P_1, P_2$, $P_m$, and $P'$, \done\todo[B15.]{I have changed this following the comment, please check.}
we have that 
$P$ is 
structurally congruent to
one of the following:
$$
\begin{array}{c}
(\nu \til{\kappa})(E\big\{C\{\inC{\kappa^{\,p}}{\til{x}}.P_1\} \para D\{\outC{\kappa^{\,\overline{p}}}{v}.P_2\}\big\}  )\\  
(\nu \til{\kappa})(E\big\{C\{\catch{\kappa^{\,p}}{x}.P_1\} \para  D\{\throw{\kappa^{\,\overline{p}}}{k^{\,q}}.P_2\} \big\}) \\
(\nu \til{\kappa})(E\big\{C\{\branch{\kappa^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} \} \para  D\{  \select{\kappa^{\,\overline{p}}}{n_i};P'\}\big\} )  \\
(\nu \til{\kappa})(E\big\{C\{\close{\kappa^{\,p}}.P_1\}  \para  D\{\close{\kappa^{\,\overline{p}}}.P_2\}\big\})
\end{array}
$$
We say a $\kappa$-redex is \emph{located} if one or both of its $\kappa$-processes is inside at least one located process.

$P$ is an \emph{error} if
$P \equiv (\nu \til{\kappa})(Q \para R)$
where, for some $\kappa$, $Q$ contains 
\underline{either} 
%exactly one $\kappa$-process
%\underline{or}
exactly 
two $\kappa$-processes that do not form a $\kappa$-redex
\underline{or}
three or more $\kappa$-processes.
\end{definition}




\subsection{Session Safety}\label{ss:safety}


We now give
subject congruence and subject reduction results for our typing discipline.
Together with some 
some auxiliary results, these provide the basis for the proof of type safety (Theorem~\ref{t:safety} in Page~\pageref{t:safety}).
We start by giving three standard results, namely weakening, strengthening, and channel lemmas.


\begin{lemma}[Weakening]
 Let $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$.  If $\mathsf{X} \notin vdom(\Theta)$ then $\judgebis{\env{\Gamma}{ \Theta,\mathsf{X}:\INT'}}{P}{\type{\ActS}{\INT}}$.
\end{lemma}
\begin{proof}
 Easily shown by induction on the structure of $P$.
\end{proof}


\begin{lemma}[Strengthening]
 Let $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$.
If $\mathsf{X}  \notin \mathsf{fv}(P)$ then $\judgebis{\env{\Gamma}{ \Theta \setminus \mathsf{X}:\INT'}}{P}{\type{\ActS}{\INT}}$.
\end{lemma}
\begin{proof}
 Easily shown by induction on the structure of $P$.
\end{proof}



\begin{lemma}[Channel Lemma]\label{lem:channel}
  Let $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$, 
 $\cha \notin \mathsf{fc}(P) \cup \mathsf{bc}(P)$ iff $\cha \notin dom(\ActS)$.
\end{lemma}
\begin{proof}
 Easily shown by induction on the structure of $P$.
\end{proof}

We are ready to show the Subject Congruence Theorem:

\begin{theorem}[Subject Congruence] \label{th:congr}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ and $P \equiv Q$ then $\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}$.
\end{theorem}
\begin{proof}
By induction on the derivation of $P \equiv Q$, with a case analysis on the last applied rule. See~\ref{app:congr} for details.\done\todo[B17.]{We have moved the proof to the appendix.}
\end{proof}

The following auxiliary result concerns substitutions for channels, expressions, and process variables.
Observe how the case of process variables has been relaxed so as to allow substitution 
with a process with ``smaller'' interface (in the sense of \intpr, cf.  Not.~\ref{n:interf}). This extra flexibility is in line
with the typing rule for located processes (rule~\rulename{t:Loc}), and will be useful later on in proofs.
%In order to prove the subject reduction theorem we need some auxiliary results. The first lemma handles substitutions.

\begin{lemma}[Substitution Lemma]\label{lem:substitution}
\quad 
\begin{enumerate}
 \item \label{subchavar}If $\judgebis{\env{\Gamma}{ \Theta}}{P}{\type{\ActS,x:\ST}{\INT}}$ then $\judgebis{\env{\Gamma}{ \Theta}}{P\sub{\cha^p}{x}}{\type{\ActS, \cha^p:\ST }{\INT}}$ %\jp{This statement should be different, I think.} \todo{check if this new formulation" is what you were thinking} 
  \item \label{subvalvar}If $\judgebis{\env{\Gamma, \til{x}:\til{\tau}}{ \Theta}}{P}{\type{\ActS}{\INT}}$ and $\Gamma \vdash \til{e}:\til{\tau}$ then $\judgebis{\env{\Gamma}{ \Theta}}{P\sub{\til{e}}{\til{x}}}{\type{\ActS}{\INT}}$. 
 % \item If $\judgebis{\env{\Gamma}{ \Theta}}{P}{\type{\ActS}{\INT}}$  then $\judgebis{\env{\Gamma}{ \Theta}}{P\sub{\cha^p}{x}}{\type{\ActS\sub{\cha^p}{x}}{\INT}}$. 
   \item \label{subprovar} If $\judgebis{\env{\Gamma}{ \Theta,\mathsf{X}:\INT}}{P}{\type{\emptyset}{\INT_1}}$ and $\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\emptyset}{\INT'}}$ with $\INT' \intpr \INT$  then, for some $\INT'_1$, we have \\ 
   $\judgebis{\env{\Gamma}{\Theta}}{P\sub{Q}{\mathsf{X}}}{\type{\emptyset}{\INT'_1}}$ with $\INT'_1 \intpr \INT_1$. %\jp{in the proof, it'd be better to explain why this inequality holds}
\end{enumerate}
\end{lemma}
\begin{proof}
Easily shown by induction on the structure of $P$.
\end{proof}

 %Then, we need to introduce how to manipulate contexts, to this aim we define the 
 \done\todo[B18.]{Some comments on "type of contexts" do not longer apply, with typed contexts.}
 As reduction may occur inside contexts, in proofs it is useful to have \emph{typed contexts},
building upon Def.~\ref{d:context}. We thus have contexts in which the hole has associated typing information---concretely, the typing for processes which may fill in the hole. Defining context requires a simple extension of judgments, in the following way:
$$
\judgebis{\mathcal{H}; \env{\Gamma}{ \Theta}}{C}{\type{\ActS}{\INT}}
$$
Intuitively, $\mathcal{H}$ contains the description of the type associated to the hole in $C$.
Typing rules in Tables~\ref{tab:ts} and~\ref{tab:session}
are extended in the expected way.
Because contexts have a single hole, $\mathcal{H}$ is either empty of has exactly one element.
When $\mathcal{H}$ is empty,
we write $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{ \INT }}$ instead of
$\judgebis{\cdot \, ; \env{\Gamma}{\Theta}}{P}{\type{\ActS}{ \INT }}$.
Two additional typing rules are required:
$$
\begin{array}{c}
\inferrule*[left=\rulename{t:Hole}] { }{\judgebis{\bullet_{\Gamma; \Theta \vdash \type{\ActS}{\INT}\,} ; \env{\Gamma}{\Theta}}{\bullet~}{\type{\ActS}{ \INT}}}		      
\\
\\
\inferrule*[left=\rulename{t:Fill}]		  
    {\judgebis{\bullet_{\Gamma; \Theta \vdash \type{\ActS}{\INT}\,} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_1}{ \INT_1 }} \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{ \INT }}} {\judgebis{\env{\Gamma}{\Theta}}{C\{P\}}{\type{\ActS_1}{ \INT_1}}}
\end{array}
$$
\noindent Axiom \rulename{t:Hole} allows us to introduce typed holes into contexts. 
In rule~\rulename{t:Fill}, $P$ is a process (it does not have any holes), and $C$ is a context with a hole of type $\Gamma; \Theta \vdash \type{\ActS}{ \INT}$. 
The substitution of occurrences of $\bullet$ in $C$ with $P$, noted $C\{P\}$ 
is sound as long as the typings of $P$ coincide with those declared in $\mathcal{H}$ for $C$.
Based on these  rules and Definitions~\ref{d:context} and~\ref{d:opcontx}, the following two auxiliary lemmas 
on properties of typed contexts follow easily. We first introduce some convenient notation for typed holes.

\begin{newnotation}
Let us use $\jug, \jug', \ldots$ to range over judgments
attached to typed holes. This way,
$\bullet_\jug$ denotes the valid typed hole associated to  $\jug = \Gamma; \Theta \vdash \type{\ActS}{\INT}$.
\end{newnotation}

%\begin{definition}[Type of contexts]
%Let $C$ be a context as in Def.~\ref{d:context}. 
%The type of $C$, denoted $\typecontx{C}{ \Gamma}{ \Theta}$, is 
%inductively defined as a pair:
%$$
%\begin{array}{ll}
% \typecontx{\bullet}{ \Gamma}{ \Theta} &= (\emptyset, \emptyset)\\
% \typecontx{\compo{l}{h}{C \para P}}{ \Gamma}{ \Theta}& = (\Pi_1( \typecontx{C}{\Gamma}{ \Theta}) \cup \ActS, ~\Pi_2(\typecontx{C}{\Gamma}{ \Theta}) \addelta \INT) \qquad \qquad \qquad \ \\
%  & \hfill \text{ if } ~\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}
%\end{array}
%$$
%where $\Pi_1(\typecontx{C}{ \Gamma}{ \Theta})$ 
%(resp. $\Pi_2(\typecontx{C}{ \Gamma}{ \Theta})$)
%denote the first (resp. second) element of pair 
%$\typecontx{C}{ \Gamma}{ \Theta}$.
%\end{definition}
%
%%\todo{Cambiare notazione $\typecontx{C}{ \Gamma}{\Theta}$}
%Next we state how to infer the type of a context:
%

A typed context may contain a typed hole in parallel with arbitrary behaviors.
This may have consequences on the typing and the interface, as 
the following lemma formalizes:

\begin{lemma}\label{lem:context}
 Let  $P$ and $C$ be a process and a typed context such that 
 $$\judgebis{\env{\Gamma}{\Theta}}{C\{P\}}{\type{\ActS}{ \INT}}$$ is a derivable judgment.
 There exist $\ActS_1, \INT_1$ such that 
 (i) $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT}_1}$ is a well-typed process, and
 (ii) $\ActS_1 \subseteq \ActS$ and $\INT_1 \intpr \INT$.
\end{lemma}
%\begin{lemma}\label{lem:context} 
% $P$ be a process and $C$ a context as in Def.~\ref{d:context}. Then \\ $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_P}{\INT_P}}$ and $\typecontx{C}{ \Gamma}{ \Theta} = (\ActS_C, \INT_C) $ iff 
%$\judgebis{\env{\Gamma}{\Theta}}{C\{P\}}{\type{\ActS_C \cup \ActS_P}{\INT_C \addelta \INT_P}}$
%\end{lemma}
%\begin{proof}
%By induction on the structure of the context $C\{\bullet\}$. The proof for the $(\Rightarrow)$ directions follows by observing that the only rules applied for typing $C\{P\}$ are  \rulename{t:Loc} and \rulename{t:Par} that either do not  change or can  only extend $\ActS_P$ and $\INT_P$. The opposite direction $(\Leftarrow)$, similarly, relies on the typing inversion on the same rules
% \rulename{t:Loc} and \rulename{t:Par}.
%\end{proof}
%%
%
%\begin{newnotation}
%In the proof of Theorem~\ref{th:subred}, we shall use the following notation 
%to denote an use of  Lemma \ref{lem:context}:
%$$
%\infer={\judgebis{\env{\Gamma}{\Theta}}{C\{P\}}{\type{\ActS_P, \ActS_C}{ \INT_P \uplus \INT_C}}}		  
%    {\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_P}{ \INT_P }}}
%$$
%\end{newnotation}




%\jp{Now I tend to think that we may need something like Lemma \ref{lem:context}. 
%The point is that in the proof we would like to get rid of contexts, justifying the ellipses (not to enclose processes within contexts, as Lemma 9 does). 
%With such a lemma, we could "go up" in the typing tree until we have something without contexts.
%At that point, we apply something (say, a substitution lemma). Then, we conclude by "going down" again, reconstructing the context. The proof would be indeed by structural induction on the context (base case: empty contexts--trivial; cases for locations/restriction are easy by IH and typing inversion).}

%\jp{Why not writing this as a corollary?}
%\todo{Maybe just a remark}
% Notice that previous lemma allows us to conclude that, given a process $P$ and a context $C$, if $\judgement{\Gamma}{\Theta}{C[P]}{\ActS}{\INT}$ then there exists $\Gamma, \Theta, \ActS', \INT'$ such that $\judgement{\Gamma}{\Theta}{P}{\ActS'}{\INT'}$.


%\todo{Subject reduction works for balanced environments; we need to introduce that notion. }

The following property formalizes the effect that a type hole has in the typing judgment of a context:
under certain conditions, 
if the typing and interface of the hole change, then the judgment for the whole context should change as well.

\begin{lemma}\label{l:ctxop}
Let $C$ be a context as in Def.~\ref{d:context}. %Then we have:
\begin{enumerate}[1.]
\item 
Suppose
$\judgebis{\bullet_\jug ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_1,k_2:\STT,\ActS'}{ \INT_1 \addelta \INT_2 \addelta \INT'}}$ 
with  $\jug = {\Gamma; \Theta \vdash \type{\ActS_1,k_2:\STT}{\INT_1 \addelta \INT_2}}$
is well-typed. 
Let  $\jug' = {\Gamma; \Theta \vdash \type{\ActS_1, k_1:\ST,k_2:\STT'}{\INT_1}}$.
Then
$$\judgebis{\bullet_{\jug'} ; \env{\Gamma}{\Theta}}{C^+}{\type{\ActS_1, k_1:\ST, k_2:\STT', \ActS'}{ \INT_1 \addelta \INT'}}$$
is a derivable judgment.

\item Suppose $\judgebis{\bullet_{\jug} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_1, k_1{:}\ST, k_2{:}\STT, \ActS'}{ \INT_1 \addelta \INT_2 \addelta \INT' }}$ with $\jug = {\Gamma; \Theta \vdash \type{\ActS_1, k{:}\ST, k_2{:}\STT}{\INT_1 \addelta \INT_2}}$
is well-typed. 
%with $\jug = {\Gamma; \Theta \vdash \type{\ActS_1, k{:}\ST, k_2{:}\STT}{\INT_1 \addelta \INT_2}}$
Let $\jug' = {\Gamma; \Theta \vdash \type{\ActS_1, k_2{:}\STT'}{\INT_1}}$.
Then %the judgment
$$\judgebis{\bullet_{\jug'} ; \env{\Gamma}{\Theta}}{C^-}{\type{\ActS_1, k_2{:}\STT', \ActS}{ \INT_1 \addelta \INT' }}$$
is a derivable judgment.

\item Suppose $\judgebis{\bullet_{\jug} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_C \cup \ActS_{\jug}}{ \INT_C \addelta \INT_{\jug} }}$ with $\jug = {\Gamma; \Theta \vdash \type{\ActS_{\jug}}{\INT_{\jug}}}$
is well-typed. 
Let $\jug' = {\Gamma; \Theta \vdash \type{\ActS_{\jug'}}{\INT_{\jug'}}}$.
Then 
$$\judgebis{\bullet_{\jug'} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_C \cup \ActS_{\jug'}}{ \INT_C \addelta \INT_{\jug'} }}$$
is a derivable judgment.
\end{enumerate}
The analogous of (1) and (2), involving 
%%Cases when the type of the hole refers to 
bracketed assignments, are as expected.
\end{lemma}

We now introduce the usual notion of \emph{balanced typing}~\cite{DBLP:journals/entcs/YoshidaV07}:

\begin{definition}[Balanced Typings]\label{d:balanced}
We say a typing 
$\ActS$ is \emph{balanced} iff 
for all $\kappa^p:\ST \in \ActS$ (resp. $[\kappa^p:\ST] \in \ActS$)
then also 
$\kappa^{\overline{p}}: \overline{\ST} \in \ActS$ (resp. $[\kappa^{\overline{p}}: \overline{\ST}] \in \ActS$).
%for all $\kappa^p:\ST \in \ActS$ then also 
%$\kappa^{\overline{p}}: \overline{\ST} \in \ActS$, and 
%for all $[\kappa^p:\ST] \in \ActS$ then also
%$[\kappa^{\overline{p}}: \overline{\ST}] \in \ActS$.
\end{definition}

The final requirement for proving safety via typing is the subject reduction theorem below.

\begin{theorem}[Subject Reduction]\label{th:subred}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced and $P \pired Q$ then 
 $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS'}{\INT'}}$, for some $\INT'$ and balanced $\ActS'$.
\end{theorem}
\begin{proof}
%%The proof proceeds by 
By induction on the last rule applied in the reduction. See~\ref{app:subred} for details.
\end{proof}


We are now ready to state our first main result:
 the \emph{absence of communication errors} for well-typed processes.
Recall that our notion of error process has been given in 
Definition~\ref{d:kred}.


\begin{theorem}[Typing Ensures Safety]\label{t:safety}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced
then $P$ never reduces into an error.
\end{theorem}

\begin{proof}
We assume, towards a contradiction, that there exists a $P_1$ 
such that ~$P \pired^* P_1$ and $P_1$ is an error process (as in~Def.~\ref{d:kred}).
By Theorem~\ref{th:subred} (Subject Reduction), $P_1$ is well-typed under a balanced typing $\D_1$.
Following Def.~\ref{d:kred}, there are two possibilities for $P_1$, namely 
it contains %(i)  exactly one $\kappa$-process, 
(i)~exactly two $\kappa$-processes which do not form a $\kappa$-redex and (ii)~three or more $\kappa$-processes.
Consider the second possibility.   
There are several combinations;
by inversion on rule \rulename{t:CRes}
we have that,
for some session types $\alpha_1$ and $\alpha_2$,
% either $\{\kappa^{p}: \alpha_1, \kappa^{\overline{p}}: \alpha_2\} \subseteq \D_1$ or  
$\{[\kappa^{p}: \alpha_1], [\kappa^{\overline{p}}: \alpha_2]\} \subseteq  \D_1$. 
In all cases, since the two $\kappa$-processes do not form a $\kappa$-redex then, necessarily, 
 $\alpha_1 \neq \overline{\alpha_2}$. This, however, contradicts the definition of balanced typings (Def.~\ref{d:balanced}).
The second possibility again contradicts Def.~\ref{d:balanced}, 
as in that case $\D_1$ would capture the fact that
at least one $\kappa$-process does not have a complementary partner for forming a $\kappa$-redex.
We thus conclude that well-typed processes never reduce to an error.
\end{proof}


\subsection{Session Consistency}\label{ss:consist}

We now investigate \emph{session consistency}: this is to 
%address a basic consequence of considering
enforce a basic discipline on 
the interplay of communicating behavior (i.e., session interactions) 
and evolvability behavior (i.e., update actions). 
Informally, %we say that a %session on channel $\kappa$ 
a process $P$
is called \emph{consistent} 
if %it is never disrupted by an evolvability step. 
%That is, 
whenever  %session on $\kappa$ is active and 
it has 
a $\kappa$-redex (cf. Def.~\ref{d:kred}) then 
possible interleaved update actions do not destroy such a redex.
%performing an update action does not affect the behavior of active sessions.

Below, we formalize this intuition. 
Let us write $P \pired_{\text{upd}} P'$ 
for any reduction inferred using rule $\rulename{r:Upd}$, possibly followed
by uses of rules $\rulename{r:Res}$, $\rulename{r:Str}$, and $\rulename{r:Par}$.
We then define:

%\begin{definition}[Session Consistency]\label{d:consist}
%Let $P$ be a process. 
%A session on channel $\kappa$ is \emph{consistent} in $P$ if,
%for all process $P', P''$ and contexts $E, C, D$ 
%such that 
%$$P \pired^{*} P' \equiv (\nu \til{\kappa})E\big\{C\{P_1\} \para  D\{P_2\}\big\}$$
%where $P_1$ and $P_2$ make $P'$ a $\kappa$-redex
%and $P' \pired_{\text{upd}} P''$, then there exist contexts $E', C'$, and $D'$ such that
%$$P'' \equiv (\nu \til{\kappa})E'\big\{C'\{P_1\} \para  D'\{P_2\}\big\}$$
%\end{definition}
%
%Hence, consistency on a session $\kappa$ %as formalized by Def.~\ref{d:consist} 
%says that update actions do not destroy $\kappa$-redexes. 
%Clearly, this definition does not rule out the possibility of interleaving intra-session communication 
%and update steps: it just requires update actions to reconfigure parts of the system not currently engaged into active sessions. 
%We find that giving priority to disciplined structured behavior over 
%runtime adaptation steps, as intended by this notion of consistency, 
%is a rather natural requirement.
%
%\jp{I feel consistency should be a property of processes, and focused on what the updates preserve
%rather than on what the sessions do. Hence I suggest stating consistency as:}

\begin{definition}[Consistency]\label{d:consis}
A process $P$ is \emph{update-consistent} 
if and only if,
 for all $P'$ and $\kappa$ 
such that $P \pired^{*} P'$ and $P'$ contains a $\kappa$-redex, 
if $P' \pired_{\text{upd}} P''$
then $P''$ contains a $\kappa$-redex.
\end{definition}

Recall that a \emph{located} $\kappa$-redex is a $\kappa$-redex in which one or both of
its constituting $\kappa$-processes are contained by least one located process.
This way, for instance, 
$$
\begin{array}{c}
\scomponent{l_2}{\,\scomponent{l_1}{\inC{\kappa^{\,p}}{\til{x}}.P_1}  \para \outC{\kappa^{\,\overline{p}}}{v}.P_2\,} \\
\scomponent{l_1}{\inC{\kappa^{\,p}}{\til{x}}.P_1}  \para \scomponent{l_2}{\outC{\kappa^{\,\overline{p}}}{v}.P_2} \\
\scomponentbig{l_1}{\inC{\kappa^{\,p}}{\til{x}}.P_1  \para \outC{\kappa^{\,\overline{p}}}{v}.P_2} 
\end{array}
$$
are located $\kappa$-redexes, whereas $\inC{\kappa^{\,p}}{\til{x}}.P_1  \para \outC{\kappa^{\,\overline{p}}}{v}.P_2$ is not.
From the point of view of consistency, the distinction between located and unlocated $\kappa$-redexes is relevant:
since update actions result from synchronizations on located processes, 
unlocated $\kappa$-redexes are always preserved by update actions, 
whereas located $\kappa$-redexes may be destroyed by a  update action.
We have the following auxiliary proposition.

\begin{proposition}\label{p:nonzero}
Let 
$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$, with $\ActS$ balanced, 
be a well-typed process containing  
a $\kappa$-redex, for some $\kappa$. We have:
\begin{enumerate}[(a)]
\item $\ActS = \ActS', \kappa^p: \ST,  \kappa^{\overline{p}}:\overline{\ST}$
~~or~~ $\ActS = \ActS', [\kappa^p: \ST],  [\kappa^{\overline{p}}:\overline{\ST}]$
, for some session type $\ST$, and a balanced $\ActS'$.
\item If the $\kappa$-redex is located, then the runtime annotation for the location(s) hosting its 
constituting $\kappa$-processes is different from zero.
\end{enumerate}

\begin{proof}
Part~(a) is immediate from our definition of typing judgment, in particular from the fact that typing $\D$
records the types of currently active sessions, as implemented by channels such as $\kappa$.
Part~(b) follows directly by definition of typing rule \rulename{t:Loc} and part (a), observing that typing relies on the cardinality of $\D$
to compute (non zero) runtime annotations for locations. 
% and the fact that $\kappa$-redexes are essentially dual active sessions recorded in $\D$.
\end{proof}

\end{proposition}

\begin{theorem}[Typing Ensures Update Consistency]\label{t:consist}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$, with $\ActS$ balanced,
then $P$ is update consistent.
\end{theorem}

\begin{proof}
%By contradiction.
We assume, towards a contradiction, that there exist $P_1$, $P_2$, and $\kappa_1$ such that
(i)~$P\pired^*P_1$, (ii)~$P_1$ has a $\kappa_1$-redex,  (iii)~$P_1 \pired_{\text{upd}} P_2$, and 
(iv)~$P_2$ does not have a $\kappa_1$-redex.  Without loss of generality, 
we suppose that the reduction $P_1 \pired_{\text{upd}} P_2$ is due to a synchronization on location $l_1 \in \T$.
Since the $\kappa_1$-redex is destroyed by the update action from $P_1$ to $P_2$, the $\kappa_1$-redex in $P_1$ must necessarily be 
 a located $\kappa_1$-redex, i.e.,  in $P_1$, one or both $\kappa_1$-processes are contained inside $l_1$.
 Now, our reduction semantics (rule \rulename{r:Upd}) decrees that for such an update action to be enabled,
 the runtime annotation for $l_1$ in $P_1$ should be zero. However, by Theorem~\ref{th:subred} (Subject Reduction), we know that $P_1$ is well-typed under a balanced
 typing $\ActS_1$. Then, using well-typedness and Prop.~\ref{p:nonzero}(b)
we infer that the annotation for $l_1$ in $P_1$ must be different from zero: contradiction. 
Hence, update steps which destroy a  
$\kappa$-redex (located and unlocated) can never be enabled from a well-typed process 
  with a balanced typing (such as $P$) nor from any of its derivatives (such as $P_1$). We thus conclude that
  well-typedness implies update consistency.
\end{proof}

%\begin{proof}[Proof (Sketch)]
%Suppose $P$ reduces to a $P'$ 
%which contains a  $\kappa$-redex. 
%Subject reduction ensures that well-typedness under balanced typings is preserved by reduction.
%Therefore, $P'$ we have 
%$\judgebis{\env{\Gamma}{\Theta}}{P'}{\type{\ActS', \kappa^p: \ST, \kappa^{\overline{p}}:\overline{\ST}}{\INT'}}$
%for some $\ST, \INT'$
%and 
%balanced typing $\Delta'$. (The assignments could be bracketed, this is for simplicity.)
%Suppose further that a reduction $P'  \pired_{\text{upd}} P''$ is enabled.
%There are two cases.
%First, the update concerns a location which does not contain none of the $\kappa$-processes.
%That is, the update is external to this $\kappa$-redex.
%We observe that the reduction to $P''$ poses no danger for the $\kappa$-processes: 
%if the update is enabled then the runtime annotation for the location 
%to be updated must be 0. Recall this annotation is maintained by typing based on $\D$.
%In fact, this update preserves \emph{all} $\kappa$-redexes in $P'$.
%Second, the update concerns a location in which one or both $\kappa$-processes are contained.
%This case is not possible:
%because typing ensures that location annotations correspond to the number of open sessions at such a location, 
%since $\kappa$-processes are declared in $\D$ the annotation for the involved location is greater than 0 and so the update cannot be enabled, because of \rulename{r:Upd}.
%\end{proof}


%We can show that all sessions in our well-typed processes are consistent. 
%We can indeed state:
%
%\begin{corollary}[Con\-sist\-ency by Typing]\label{cor:cons}
%Suppose %\\%$P$ be a well-typed process. 
%$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} $
%is a well-typed process.
%Then every session $\ST_\qua \in \INT$ %that can be established along the evolution of $P$, we have that 
%is consistent, in the sense of Def.~\ref{d:consist}.
%\end{corollary}
%
%This result follows from Thm.~\ref{th:subred} 
%by observing that 
%enabling update actions only for 
%located processes without active sessions (cf. rule \rulename{r:Upd}), essentially 
%rules out the possibility of 
%updating a location containing 
%a communicating process $P_{\langle c \rangle}$, as defined above.
%Indeed, our type system ensures that the annotations enabling update actions 
%are correctly assigned and maintained along reduction.




% 
 \section{Example: An Adaptable Client/Service Scenario}\label{sec:exam}

%\newpage
To illustrate how
located and update processes
in our framework extend the expressiveness of session-typed languages, we  
revisit the  client/server scenario discussed in the Introduction:
% of distributed, interacting services (a client $C_1$ and a replicated service $S$), 
%conveniently represented as located processes:
\begin{eqnarray*}
\mathsf{Sys} & \triangleq &  %\scomponent{l_{0}}{C_1} \para 
%\scomponent{l_{1}}{C_1} \para\bigscomponent{l_2}{\scomponent{r}{S} \para R \, } \quad\text{where:} \vspace{3mm} \\ 
%C_1  &  \triangleq  & \nopenr{a}{c:\overline{\ST}}.\outC{c}{u_1,p_1}.\select{c}{n_1.P_1}.\close{c} \\
%S  &  \triangleq  & \repopen{a}{s:\ST}.\inC{s}{u,p}.\branch{s}{n_1{:}Q_1 \parallel n_2{:}Q_2}.\close{s} 
\scomponent{l_{1}}{C_1} \para\bigscomponent{l_2}{\scomponent{r}{S} \para R \, } \quad\text{where:} \vspace{3mm} \\ 
C_1  &  \triangleq  & \nopenr{a}{x}.\outC{x}{\mathrm{u_1},\mathrm{p_1}}.\select{x}{n_1.P_1}.\close{x} \\
S  &  \triangleq  & \repopen{a}{y}.\inC{y}{u,p}.\branch{y}{n_1{:}Q_1.\close{y} \alte n_2{:}Q_2.\close{y}} 
\end{eqnarray*}
%Intuitively, 
%$\mathsf{Sys}$ 
%consists of a server $S$ and a client $C_1$.
%They 
%may interact by establishing a session %of type $\sigma$ 
%%between $S$ and $C_1$ %($i \in \{0, 1\}$) 
%using name $a$:
%first, the client sends its user credentials to the server; then, the client chooses one of the two
%services offered by the server. 
%Above, the actual client and server behaviors are  abstracted by processes $P_1$ and $Q_1$, respectively,
%%(resp. $P_1$ and $Q_1$), 
%which are left unspecified.
%Finally, server and client synchronize to close the session.

Recall that process $R$ above represents the platform in which service $S$ is deployed.
We now discuss two
different definitions for $R$:
this is useful to illustrate  the different facets that runtime adaptation may adopt in our typed framework.

In what follows, we assume that $Q_i$ realizes a  behavior denoted by type $\beta_i$ ($i \in \{1,2\}$),
and write $\alpha$ to stand for the session type $?(\tau_1,\tau_2).\&\{n_1: \beta_1, n_2: \beta_2\}$ for the server $S$.
Dually, the type for $C_1$ is $\overline{\alpha} = !(\tau_1,\tau_2).\oplus\{n_1: \overline{\beta_1}, n_2: \overline{\beta_2}\}$;
we assume that $P_1$ realizes the session type  $\overline{\beta_1}$.
  
  
%\todo{change $c, s$ with $x$ and say what's $\alpha$.}

\subsection{A Basic Service Reconfiguration: Relocation and Upgrade}
%Here we develop an $R$ which keeps the distributed structure, but adds another service to the menu.
We first suppose that $R$ stands for a simple adaptation routine for $S$ which 
(i)~relocates the service from $r$ to $l_4$, and 
(ii)~sets up a new adaptation routine at $l_4$ which upgrades $S$ with adaptation mechanisms for $Q_1$ and $Q_2$ (denoted $R_{11}$ and $R_{12}$, respectively, and left unspecified):
\begin{eqnarray*}
R & \triangleq &  \adapt{r}{ \scomponent{l_4}{\mathsf{X}}   \para \adapt{l_4}{\scomponent{l_4}{S_{\text{new}}}}{\mathsf{X}_1} \, }{\mathsf{X}}~ \qquad\text{where:} \\
S_\text{new}  &  \triangleq  & \repopen{a}{y}.\inC{y}{u,p}.\branch{y}{n_1{:}Q^*_1.\close{y} \alte n_2{:}Q^*_2.\close{y}\,}  \\
Q^*_1 & \triangleq &  \scomponent{l_5}{Q_1} \para \adapt{l_5}{R_{11}}{\mathsf{X}_2} \\
Q^*_2 & \triangleq &  \scomponent{l_6}{Q_2} \para \adapt{l_6}{R_{12}}{\mathsf{X}_3}
\end{eqnarray*}
It is easy to see that the only difference between $S$ and $S_\text{new}$ is in the behavior given at label $n_2$---for 
simplicity, we assume that $Q_2$ and $Q^*_2$ are implementations of the same typed behavior.
For this $R$, using our type system, we can infer that 
$$
\judgebis{\env{\Gamma}{\Theta}}{\mathsf{Sys}}{\type{\emptyset}{\INT_1}} \qquad \text{where:}
$$

\begin{itemize}
\item $\{ a: \langle \ST_\quau, \overline{\ST}_\qual \rangle \} \subseteq \Gamma$
\item $\{ l_1\mapsto a:\overline{\ST}_\qual,~ 
l_4\mapsto a:\ST_\quau, ~ r\mapsto a: \ST_\quau , ~ \mathsf{X} \mapsto a: \ST_\quau  \} \subseteq \Theta$
\item $ \INT_1 = \{ \qual\,a:\overline{\ST},  ~ \quau\,a:\ST \} $ %CHECK HERE
\end{itemize}
and where we have\done\todo[B39.]{Fixed, pls check} slightly simplified notation for $\Theta$, for readability reasons.

By virtue of Theorem~\ref{t:safety}
typing ensures communications between $C_1$ and $S$ which follow the prescribed session types. Moreover, 
by relying on Theorem~\ref{t:consist}, we know that well-typedness implies consistency, i.e., % between $C$ and $S$, i.e., 
an update action on  $r$ will not be enabled if $C_1$ and $S$ have already initiated a session.
For the scenario above, 
our typed framework ensures that  updates may only take place before a session related to the service on $a$ is established.
Suppose such an action occurs as the first action of $\mathsf{Sys}$ (i.e. service $S$ is immediately relocated, from $r$ to $l_4$): 
$$
\mathsf{Sys} \pired 
%\component{l_{0}}{0}{}{C_0} \para
\component{l_{1}}{0}{}{C_1} \para 
\bigcomponent{l_2}{0}{}{\component{l_4}{0}{}{S}  \para \adapt{l_4}{\scomponent{l_4}{S_\text{new}}}{{\mathsf{X}_1}} \,} 
%\pired \component{l_{0}}{0}{}{C_0} \para \component{l_{1}}{0}{}{C_1} \para \bigcomponent{l_2}{0}{}{\component{l_4}{0}{}{S_\text{new}}  \,}  
= \mathsf{Sys}_1
$$
The above reduction represents one of the simplest forms of reconfiguration, one in which the behavior of the located process
is not explicitly changed. 
Still, we observe that runtime relocation may \emph{indirectly}\done\todo[B40.]{Fixed, pls check} influence the future behavior of a process.
For instance, after relocation the process may 
synchronize with reconfiguration routines (i.e., update processes) not defined for the previous location.
This is exactly what occurs with the above definition for $R$ when relocating $S$ to $l_4$---see below.\footnote{
Conversely, 
update actions that 
remove the enclosing location(s) for a process, or 
relocate it to a location on which there are no update processes available are two ways of preventing future updates.}
Also, the new location may be associated to a larger interface (wrt $\sqsubseteq$) and this could be useful to eventually
enable reconfiguration steps not possible for the process in the old location.

Starting from $\mathsf{Sys}_1$, the service $S$ can be then upgraded to $S_\text{new}$ by synchronizing on $l_4$. We may have:
$$
\mathsf{Sys}_1 
%\pired \component{l_{0}}{0}{}{C_0} \para \component{l_{1}}{0}{}{C_1} \para \bigcomponent{l_2}{0}{}{\component{r_1}{0}{}{S_\text{new}}  \para \adaptn{r}{\scomponent{l_4}{\mathsf{X}}} \,} 
\pired %\component{l_{0}}{0}{}{C_0} \para 
\component{l_{1}}{0}{}{C_1} \para \bigcomponent{l_2}{0}{}{\component{l_4}{0}{}{S_\text{new}}  \,}  = \mathsf{Sys}_2
$$
and by Theorem~\ref{th:subred} we infer that 
$$
\judgebis{\env{\Gamma}{\Theta}}{\mathsf{Sys}_2}{\type{\emptyset}{\INT_1}}
$$

\subsection{Upgrading Behavior and Distributed Structure}\label{ss:behdist}
Suppose now that $R$ stands for the following adaptation routine for $S$:
$$
\begin{array}{ll}
R & \triangleq   \adapt{r}{\scomponent{r_1}{S_\text{wra}}  \para \scomponent{r_2}{S_\text{rem}} }{{\mathsf{X}}}~ \qquad\text{where:} \\
%S_\text{wra}  &  \triangleq  & \repopen{a}{s:\ST}.\nopenr{b}{d:!(\ST)}.\throw{d}{s}.\close{d} \\
%S_\text{rem} &  \triangleq  &  \repopen{b}{e:?(\ST)}.\catch{e}{s}.\inC{s}{u,p}.\branch{s}{n_1{:}Q_1 \parallel n_2{:}Q_2}.\close{s}.\close{e} 
S_\text{wra} \! \! \! \!&  \triangleq   \repopen{a}{x}.\nopenr{b}{y}.\throw{y}{x}.\close{y} \\
S_\text{rem} \! \! \! \!&  \triangleq    \repopen{b}{z}.\catch{z}{x}.\inC{x}{u,p}.\branch{x}{n_1{:}Q_1.\close{x}.\close{z}  \alte %\\
%& 
%\qquad \qquad \qquad \qquad \qquad \qquad  \quad \qquad 
n_2{:}Q_2.\close{x}.\close{z} }
\end{array}
$$
Above, $S_\text{wra}$ represents a service wrapper which, deployed at $r_1$, acts as a mediator: 
it redirects all client requests on name $a$ 
to the remote service $S_\text{rem}$, defined on name $b$ and deployed at $r_2$. 
Although simple, this service structure is quite appealing: 
by exploiting session delegation, 
it hides 
from clients certain implementation details (e.g.,  name $b$ and location $r_2$), 
therefore simplifying  future reconfiguration tasks---in fact, clients do not need to know about $b$ to execute, and so $S_\text{wra}$ can be transparently upgraded.
This new definition for $R$ illustrates\done\todo[B41.]{Fixed, pls check} an update process that may reconfigure both
the behavior and distributed structure of $S$:
in a single step, 
the monolithic service $S$ is replaced by a more flexible distributed
implementation based on  $S_\text{wra}$ and $S_\text{rem}$ and deployed at $r_1$ and $r_2$ (rather than at $r$).
As we discuss below, $R$ above does not involve process variables, and so the current behavior at $r$ is discarded.
Using our type system, we may infer that 
$$
\judgebis{\env{\Gamma}{\Theta}}{\mathsf{Sys}}{\type{\emptyset}{\INT_1}} \qquad \text{where:}
$$

\begin{itemize}
\item $\{ a: \langle \ST_\quau, \overline{\ST}_\qual \rangle,~  
b: \langle !(\ST)_\qual, ?(\ST)_\quau \rangle \} \subseteq \Gamma$
\item $\{ l_1\mapsto a:\overline{\ST}_\qual,~ 
l_2\mapsto a:\ST_\quau \cup b: !(\ST)_\quau \cup b: ?(\ST)_\quau, ~
r\mapsto a: \ST_\quau, ~ 
r_1\mapsto \ST_\quau \cup b: !(\ST)_\quau,~ \\
r_2\mapsto b: ?(\ST)_\quau
\} \subseteq \Theta$
\item $ \INT_1 = \{  \qual\,a:\overline{\ST},  ~ \quau\,a:\ST \} $ %CHECK HERE
\end{itemize}
and where we have\done\todo[B42.]{Fixed, pls check} slightly simplified notation for $\Theta$, for readability reasons.

As before,  our typed framework ensures that 
consistent updates may only take place before a session related to the service on $a$ is established.
Suppose such an action occurs as the first action of $\mathsf{Sys}$ (i.e. the definition of service $S$ is immediately updated): %before a session on $a$ is established. 
$$
\mathsf{Sys} \pired 
%\component{l_{0}}{0}{}{C_0} \para
\component{l_{1}}{0}{}{C_1} \para \bigcomponent{l_2}{0}{}{\component{r_1}{0}{}{S_\text{wra}}  \para \component{r_2}{0}{}{S_\text{rem}}} = \mathsf{Sys}'
$$
Because $R$ declares no process variables, this step
formalizes an update operation which \emph{discards} the behavior located at $r$ (i.e., $a: \alpha_\quau$).
To understand why this reconfiguration step is safe, it is crucial to observe that:
\begin{enumerate}[(i)] 
\item  the new service implementation, based on $S_\text{wra}$ and $S_\text{rem}$, respects the prescribed interfaces of the involved locations (i.e., $r_1$ and $r_2$, not used in $\mathsf{Sys}$); 
\item  the interface of location $l_2$ (which hosts the server implementation) can indeed contain the two services on name $b$ implemented by $S_\text{wra}$ and $S_\text{rem}$.
\end{enumerate}
These two important conditions are statically checked by our typing system.
After the reduction it is easy to see that 
$$
\judgebis{\env{\Gamma}{\Theta}}{\mathsf{Sys}'}{\type{\emptyset}{\INT_2}} 
$$
where $\Gamma, \Theta$ are as above and $\INT_2 = \{ \qual \, a:\overline{\ST},~\quau \, a:\ST,~\quau \, b: ?(\ST), ~\quau \, b: !(\ST)\}$.
We have $\INT_1 \sqsubseteq \INT_2$: indeed the interface grows as \done\todo[B43.]{Fixed as suggested, pls check}the updated service  now relies on two service definitions (on names $a, b$) rather than on a single  definition.

%\jp{Other ideas for extending the example?}


%\subsection{More interesting server}
%
%
%We consider the interaction between a Client and a Server as the process $S \parallel C$. 
%The behavior of the server is encoded trough an adaptable process that recursively establishes new sessions with clients:
%$$ S ::= \component{s}{0}{\Delta}{\rec{X:\emptyset, \Delta}{(\open{c:\rho}.c(x).\close{c} \parallel X)} }$$ 
%where $\Delta= \emptyset \shortmid \{\rho\}$ and $\rho = ?(int).\epsilon$.
%
%Clients, in order to connect to the server, must implement a session that is the dual of the one described above: 
%$$C ::= \open{c:\overline{\rho}}.\outC{c}{e}.\close{c}$$
%where $e$ is an expression that evaluates to  $int$.
%
%We now extend this scenario introducing a way of updating the server: $S \parallel C \parallel U$. Here, the update $U$ is meant to extend  the capabilities (for instance by enhancing its performance) of the server by adding an auxiliary machine $M$. The server is then delegating its sessions to $M$:
%$$
%\begin{array}{ll}
%U ::= & \updated{s}{X}{\Delta}{\Delta}{(\component{s}{0}{\Delta}{\rec{X:\emptyset, \Delta}{(\open{c:\rho}.\\
%& \qquad \qquad \open{d:\sigma}.\throw{d}{c}.\close{d}} \parallel X)} \parallel M)}\\
%M ::= &\component{m}{0}{\Delta'}{\rec{X:\emptyset, \Delta'}{(\open{d:\overline{\sigma}}.\catch{d}{e}.\\
%&  \qquad \qquad e(x).\close{e}.\close{d} \parallel X)}}
%\end{array}
% $$
%where $\Delta' = \emptyset \shortmid \ \{\overline{\sigma}\}$ and $\sigma = !(\rho).\epsilon$.




  

%T = open 
% 
% \section{Discussion: Towards More Flexible Interfaces}\label{sec:int}
% \input{interface}
 
 \section{Extensions and Enhancements}\label{sec:disc}
%A brief discussion on when locations with open/running sessions can be updated.
%We could exploit the "preserving" class of updates defined in the LMCS paper.


This section discusses two possible extensions for our framework.
The first one concerns the runtime adaptation 
of processes with active (running) sessions, while the second one concerns the inclusion of recursion and subtyping constructs.
In both cases,  concrete details on the technical machinery required are given, and   the challenges involved are highlighted.

\subsection{Runtime Adaptation of Processes with Active Sessions}
Up to here, our notion of runtime adaptation concerns located processes with no active sessions. 
As already motivated, our intention is to rule careless update actions which may affect the session protocols implemented on such locations.
Here we discuss generalizations of our framework so as to admit the runtime adaptation of located processes containing active sessions. As before, the goal will be to ensure that session communications are %never disrupted by update actions.
both safe and consistent.

To illustrate this point, consider  process $\mathsf{Sys}'$, discussed in the Introduction:
\begin{eqnarray*}
\mathsf{Sys}' \!\!\!& = & \!\!\!\! (\nu \kappa)\big(\scomponent{l_{1}}{\outC{\kappa^{+}}{\mathrm{u_1},\mathrm{p_1}}.\select{\kappa^{+}}{n_1.P_1}.\close{\kappa^{+}}} \para \\ 
& & \qquad \quad \bigscomponent{l_2}{\scomponent{r}{\inC{\kappa^{-}}{u,p}.\branch{\kappa^{-}}{n_1{:}Q_1.\close{\kappa^{-}} \alte n_2{:}Q_2.\close{\kappa^{-}}}\,} \para R \, }\big)
\end{eqnarray*} 

%Consider a located process $\scomponent{l}{P} $ 
\noindent Focusing on location $r$, suppose that 
%and an associated adaptation routine 
$R = \adapt{r}{Q_{\mathsf{X}}}{\mathsf{X}}$.
%Suppose that $P$ contains already established sessions.
There are at least two ways in which $Q_{\mathsf{X}}$ can implement a consistent update on $r$:
\begin{enumerate}[(a)]
\item $Q_{\mathsf{X}}$ \emph{preserves} the behavior at $r$: Intuitively, this means that  $\mathsf{X}$ occurs linearly (exactly once)
in $Q_{\mathsf{X}}$. This way, $Q_{\mathsf{X}}$ may implement a relocation  (as in, e.g., $Q_{\mathsf{X}} = \scomponent{l'}{\mathsf{X}}$, for some different location $l'$) or it may place the behavior at $r$ in a richer context (as in, e.g.,  $Q_{\mathsf{X}} = \scomponent{r}{\mathsf{X} \para R'}$ in which the behavior at location $r$ is \emph{extended} with process $R'$).

\item $Q_{\mathsf{X}}$ \emph{upgrades} the behavior at $P$: This is the case when, e.g., %Intuitively, this means that 
%entails that $Q_{\mathsf{X}} = \scomponent{l}{P'}$ and variable $\mathsf{X}$ does not occur in $P'$. 
$\mathsf{X} \not\in \mathsf{fpv}(Q_{\mathsf{X}})$.
In order to ensure consistency, besides ensuring a compatible interface, the new behavior $Q_{\mathsf{X}}$ should implement all open sessions at $r$ (namely $\kappa^{-}, \kappa^{+}$ above). Therefore, this possibility implies having precise information on the  protocols implemented at $r$, 
for $Q_{\mathsf{X}}$ must continue with such protocols.
\end{enumerate}

%In the rest of the section, we discuss 
\noindent Next we separately consider each of these two alternatives.
%giving technical details on how they 
% can be incorporated in our framework (assuming syntax and typing rules without runtime annotations).
%with running sessions, there are basically two approaches to ensure session consistency: i) the process $P$ is preserved by the update $\adapt{l}{Q}{X}$, i.e., $\mathsf{X}$ appears in $Q$  or ii) a mechanism is needed to share session channels between the process $P$ and the process $Q$. 


\subsubsection{Typing Preserving Updates}\label{ss:pres}
As mentioned above, the key issue in this class of updates is 
%The goal of such restrictions is 
to ensure \emph{linearity} of the processes variable.
Given $\adapt{l}{Q_{\mathsf{X}}}{\mathsf{X}}$, we need to 
guarantee that $\mathsf{X} \in \mathsf{fpv}(Q_{\mathsf{X}})$ (to avoid  discarding the behavior at $l$)
but also that $\mathsf{X}$ occurs exactly once, for duplicating behaviors would be unsound.
A first, but somewhat drastic, way of ensuring linearity would be by adding syntactic restrictions on the shape of 
update contexts (such as  $Q_{\mathsf{X}}$).
We have formalized this alternative is in~\cite[\S\,2.1.2]{BGPZFMOODS}, where behavioral characterizations of update processes are thoroughly analyzed.

%The first strategy is easy to implement, one possible but drastic solution is to require some syntactic restriction on the form of $Q$.
%Notice that not only we require to preserve the process $P$, thus $\mathsf{X} \in \mathsf{fpv}(Q)$,  but we also expect to have  only one occurrence of $\mathsf{X}$ in $Q$ as it would not be reasonable to duplicate behaviors. 
Alternatively, we could exploit the type system, using the information in $\Theta$ to ensure linearity.
%so that exactly one occurrence of $\mathsf{X}$ occurs in $Q$. 
This would require changing rule~\rulename{t:Nil} so that $\nil$ can only be typed in a higher-order environment that contains no process variables.
Also, one would need to refine rule~\rulename{t:Par} so to ensure that process variables are properly split.
More precisely, we would need the following modified rules:
%in $\Theta$ are partitioned among $\Theta_1$ and $\Theta_2$:
$$
\begin{array}{c}
\inferrule*[left=\rulename{t:LNil}]{vdom(\Theta)=\emptyset}{\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}}
\\ \\
\inferrule*[left=\rulename{t:LLoc} ]
 {
       \Theta \vdash l:\INT \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } }   \qquad \INT' \intpr \INT
 }{\judgebis{\env{\Gamma}{\Theta}}{\component{l}{}{\INT}{P} }{ \type{\ActS}{\INT' }}}
\\ \\
 \inferrule*[left=\rulename{t:LPar}]
 { \judgebis{\env{\Gamma}{\Theta_1}}{P}{\type{\ActS_1}{ \INT_1}} \qquad \judgebis{\env{\Gamma}{\Theta_2}}{Q}{ \type{\ActS_2}{ \INT_2}} \qquad \Theta = \Theta_1 \circ \Theta_2
%  \begin{array}{c}
%\judgebis{\env{\Gamma}{\Theta_1}}{P}{\type{\ActS_1}{ \INT_1}} \qquad
% \judgebis{\env{\Gamma}{\Theta_2}}{Q}{ \type{\ActS_2}{ \INT_2}} \\ \Theta = \Theta_1 \cup \Theta_2 \quad vdom(\Theta_1) \cap vdom(\Theta_2) = \emptyset
%\end{array}
 }{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT_1 \addelta \INT_2}}}
 \end{array}
$$
where, in $\rulename{t:LPar}$, the splitting 
$\Theta_1 \circ \Theta_2$ is defined if and only if 
$\Theta_1 \cap \Theta_2 = \emptyset$ and $ vdom(\Theta_1) \cap vdom(\Theta_2) = \emptyset$.
Observe that the interplay of these two rules %\rulename{t:Nil'} and \rulename{t:Par'} 
suffices 
to guarantee linearity of process variables.
%that exactly one occurrence of $\mathsf{X}$ occurs in $Q$. 
Indeed, rule~\rulename{t:LPar} ensures that variable $\mathsf{X}$ can be used in at most one subprocess in parallel, whereas rule~\rulename{t:LNil} assures that it is used at least one. Notice also that we keep rule~\rulename{t:Adapt}
as in Table~\ref{tab:ts}: its right-hand side typing ensures that the context does not introduce new open sessions.

With these changes in the typing system, 
the runtime annotation on the number of active sessions (occurring in located process)
can be removed from the reduction semantics. The modified semantics can be found in~\ref{ap:addmat}~(Table \ref{tab:semanticsnoannot}).
% we guarantee that no other open session is introduced in $Q$. 
 
\subsubsection{Typing Runtime Upgrades}
 We now generalize the mechanism in the  previous section to include the \emph{runtime upgrade} of a process $\scomponent{l}{P}$  with a process $Q$ that in particular provides an alternative implementation for the active protocols in $P$. 
As explained earlier, handling an upgrade entails having precise knowledge on the protocols running in the location. 
More precisely, a main challenge is to find a way of %sharing active session 
describing compatibility between the (non bracketed)
endpoints  in $P$ with those in $Q$. We now detail a  possible solution to these issues, based on %handle such knowledge is to introduce a proper reduction 
%defining a typed reduction semantics, 
instrumenting the reduction semantics in \S\,~\ref{ss:opsem} with typing environments. %information. 
Let us consider \emph{typed reductions} of the form:
$$
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} 
\pired 
\judgebis{\env{\Gamma}{\Theta}}{P'}{\type{\ActS'}{\INT'}} 
$$
thus defining how a well-typed process $P$ (and their associated typing and interface) evolve as a result of an internal computation.
We now discuss some selected rules for this typed semantics, given in Table~\ref{tab:selected}; the complete set of rules can be found in~\ref{ap:addmat} (Tables \ref{tab:1typedsemantics} and \ref{tab:typedsemantics}).  

 \begin{table}[t]
 $$
 \begin{array}{lc}
 \rulename{r:ParU}&
 \infer{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{ \type{\ActS_1 \cup \ActS_2}{\INT_1 \cup \INT_2 }} \pired \judgebis{\env{\Gamma}{\Theta}}{P' \para Q}{ \type{\ActS_1' \cup \ActS_2}{\INT_1' \uplus \INT_2' }}}{ \judgebis{\env{\Gamma}{\Theta}}{P }{ \type{\ActS_1}{\INT_1 }} \pired \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS_1'}{\INT_1' }}}
  \\ \\
  \rulename{r:LocU}&
 \infer{\judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P}}{ \type{\ActS}{\INT }} \pired \judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P'}}{ \type{\ActS'}{\INT'}}}{\judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS}{\INT }} \pired \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS'}{\INT'}} }
 \\ \\
 \rulename{r:UpdU}&
\infer{
\begin{array}{c}
\judgebis{\env{\Gamma}{\Theta}}{C\{\scomponent{l}{P}\} \para  D\{\adapt{l}{Q}{X}\}}{\type{\ActS}{\INT}} \\
 \pired \\ %\qquad  \qquad \qquad  \qquad  \\ \qquad  \qquad 
\judgebis{\env{\Gamma}{\Theta}}{C\{\rho(Q)\sub{P}{\mathsf{X}}\}  \para  D\{\nil\}}{\type{\ActS}{(\INT \setminus \INT_1) \uplus \INT_2}}
\end{array}
}
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{\INT_1}} \qquad \judgebis{\env{\Gamma}{\Theta, \mathsf{X}:\ActS_1,\INT_1}}{Q}{\type{\ActS_2}{\INT_2}} \qquad \ActS_1 = \rho(\ActS_2)}
\\ \\
&  
 \judgebis{\env{\Gamma}{\Theta}}{C\{\nopena{a}{x}.P\} \para D\{\nopenr{a}{y}.Q\}}{ \type{\ActS}{\INT, a:\alpha_{\qual}, a:\overline{\alpha}_{\qual} }}  \\
\rulename{r:OpenU} & \pired \\
&    \judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{C\{P\sub{\cha^+}{x}\} \para D\{Q\sub{\cha^-}{y}}\}}{ \type{\ActS,[\cha^+:\alpha],[\cha^-:\overline{\alpha}]}{\INT}}
 \end{array}
 $$
 \caption{Typed reduction semantics (selected rules).}\label{tab:selected}  
 \end{table}


Main differences with respect to the semantics of Table~\ref{tab:semantics} are:
(i) runtime annotations on locations are no longer needed, and 
(ii) rule $\rulename{r:UpdU}$ checks session consistency by appealing to appropriate typings (denoted $\ActS_1$ and $\ActS_2$ in the rule).
More precisely, as runtime annotations are not considered, typed reduction rules are simpler than untyped ones.
Notice how rule~\rulename{r:LocU} allows us to infer reductions with a single location; 
in general, given a context $C$ (as in Def.~\ref{d:context}) and a process $P$ which may reduce, 
a corresponding typed reduction for process $C\{P\}$  can be inferred by combining rules~\rulename{r:LocU} and \rulename{r:ParU}.
%a filled context can be reduced by the combination of rules  and
Rule \rulename{r:UpdU} 
concerns the update of a located process $P$ with a context $Q$. A typed update reduction will depend on their associated typings, denoted $\ActS_1$ and $\ActS_2$, respectively.
%allows us to replace only processes where the active sessions in $P$ can be matched by the process $Q\sub{P}{\mathsf{X}}$. 
Intuitively, $\ActS_1$ and $\ActS_2$ should be identical, up to a substitution $\rho$ from channel variables $x_1, \ldots, x_m$ in $\ActS_2$
to non bracketed channels $\cha_1^p, \ldots, \cha_m^p$ in $\ActS_1$. 
Substitution $\rho$ works then as an adaptor; to highlight its role, in rule~\rulename{r:UpdU}  we write $\rho(\ActS)$ and $\rho(P)$ to denote the application of $\rho$ to typing $\ActS$ and process $P$; the formal definition of these notations is as expected.
This is how endpoint compatibility between $P$ and $Q$ is enforced. Provided a suitable $\rho$ exists, the 
%To this end, the rule checks whether there exists a suitable assignment $\rho$ such that  type $\ActS_P$ (of active sessions in $P$) matches the type of active sessions in $Q\sub{P}{\mathsf{X}}$: i.e., $\ActS_P = \ActS_Q[\rho]$. If this is the case, the 
upgrade can take place and $\scomponent{l}{P}$ is substituted with  $\rho(Q)\sub{P}{\mathsf{X}}$.


%We start by introducing an assignment function $\rho$ that matches each channels variable $x$ to a channels name $\kappa$,  $\rho$ is used to substitute channel variables in typings $\Delta$ and in processes:  $\Delta[\rho]$ is inductively defined as follows: 
%$$
%\begin{array}{lcl}
% \emptyset[\rho] & =  &\emptyset\\
% (\Delta, \kappa^p:\alpha)[\rho] & = & \Delta[\rho], \kappa^p:\alpha\\
% (\Delta, [\kappa^p:\alpha])[\rho] & = & \Delta[\rho], [\kappa^p:\alpha]\\
% (\Delta, x:\alpha)[\rho] & = & \Delta[\rho], \kappa':\alpha \text{ with } (x,\kappa') \in \rho  
%\end{array}
%$$
%and given a process $P$, $P[\rho]$ represent the systematic substitution of assignments in $\rho$ to process $P$ (i.e., let $\rho = \{(x_1, \kappa_1)\dots (x_n, \kappa_n)\}$ then $P[\rho]=P\sub{x_1}{\kappa_1}\dots\sub{x_n}{\kappa_n}$).

For the system with the typed reduction semantics, we require the   
%is the adaptation of the reduction semantics in Table \ref{tab:semantics} with the 
typing rules in Tables~\ref{tab:ts} and~\ref{tab:session}, replacing rules \rulename{t:Pvar}, \rulename{t:Adapt} and \rulename{t:Loc} with rules  \rulename{t:PVarU}, \rulename{t:AdaptU} and \rulename{t:LocU} below:
$$
\begin{array}{c}
 \inferrule*[left=\rulename{t:PVarU}]{ }{\Gamma; \Theta,\mathsf{X}:\type{\ActS}{\INT} \vdash \mathsf{X}:\type{\ActS}{\INT}}\\ \\

 \inferrule*[left=\rulename{t:AdaptU} ]
{\Theta \vdash l:\INT  \qquad  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:\type{\emptyset}{\INT}}}{P}{\type{\ActS}{ \INT }}}{\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{\mathsf{X}}}{\type{\emptyset}{ \emptyset}}} \\ \\

\inferrule*[left=\rulename{t:LocU} ]
 {
       \Theta \vdash l:\INT \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } }   \qquad \INT' \intpr \INT
 }{\judgebis{\env{\Gamma}{\Theta}}{\component{l}{}{\INT}{P} }{ \type{\ActS}{\INT' }}}
\end{array}
$$

Intuitively, as made explicit by rule~\rulename{t:PVarU}, process variables must now record both a typing $\ActS$ and an interface $\INT$. This refines the intrinsic meaning of an update operation, as there is an explicit reference to required open sessions. 
Based on this enhancement, rule~\rulename{t:AdaptU} is a variant  of rule~\rulename{t:Adapt} in which the process variable occurs annotated with its typing and interface and where we admit a non empty typing $\ActS$, thus allowing process $P$ to introduce active sessions.
Finally, rule~\rulename{t:LocU} simplifies rule~\rulename{t:Loc} by eliminating runtime annotations.
We are confident that session processes in this modified framework also enjoy our safety and consistency results 
(Theorems~\ref{th:subred},~\ref{t:safety}, and \ref{t:consist}) 
 with little modifications.
 %, for the enhanced typed systems and semantics for both preserving and runtime updates. 
% As a consequence we can ensure that a well typed process does not disrupt active communications along its evolution.
 
 

 


 \subsection{Adding Recursive Types and Subtyping}\label{sec:recsub}
\newcommand{\unf}[1]{\ensuremath{\mathbf{unfold}(#1)}}
\newcommand{\mcc}[1]{\ensuremath{\mathcal{#1}}}
\newcommand{\ty}{\ensuremath{T}}
\newcommand{\tyy}{\ensuremath{S}}
\newcommand{\bsub}{\ensuremath{\leq_{\mathtt{B}}}\xspace}
\newcommand{\csub}{\ensuremath{\leq_{\mathtt{C}}}\xspace}
\newcommand{\cdual}{\ensuremath{\,\bot_{\mathtt{C}}}\,}

This section discusses the extension of our approach 
with \emph{recursive types} and \emph{subtyping}.
These are two well-known ingredients of session type theories:
while recursion is present in early papers in binary session types~\cite{DBLP:conf/esop/HondaVK98},
subtyping was first studied by Gay and Hole in~\cite{DBLP:journals/acta/GayH05}.
Notice that 
by extending the types in Table~\ref{tab:types}  
with recursive types we obtain a type syntax that coincides with that in~\cite{DBLP:conf/esop/HondaVK98,DBLP:journals/entcs/YoshidaV07},
and is quite similar to that in~\cite{DBLP:journals/acta/GayH05}. 
As such, 
the incorporation of both recursive types  and subtyping closely follows prior works, 
and entails unsurprising technical details.
Still, the extension is interesting: on the one hand, recursive types increase the expressiveness of our language; on the other, 
subtyping allows us to refine the notion of interface (and interface ordering), thus enhancing our typed constructs for runtime adaptation.


\subsubsection{Extended Process and Type Syntax}\label{ss:extproc}
We begin by re-defining the process language. 
Consider an additional base set of \emph{recursion variables},
ranged over $\rv Y, \rv Y',\ldots$. 
In essence, we consider the language in 
Table~\ref{tab:syntax} without replicated session acceptance and with the addition of \emph{recursive calls}, denoted $\recu\,\rv Y. P$:
\begin{align*}
P, Q, R  ::= ~~ &   \nopenr{a}{x}.P   \sepr   \nopena{a}{x}.P \\
 \sepr &  \outC{k}{\tilde{e}}.P \sepr    \inC{k}{\tilde{x}}.P   
	  \sepr    \throw{k}{k'}.P \sepr    \catch{k}{x}.P   \\
	\sepr &  \select{k}{n};P \sepr   \branch{k}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} \sepr \close{k}.P  \sepr   \restr{k}{P} \\
	\sepr &  \scomponent{l}{P}    	\sepr   \adapt{l}{P}{\mathsf{X}}  	     \sepr    \mathsf{X}  \sepr \recu\,\rv Y. P \sepr \rv Y \\
	\sepr &   P \para  P  \sepr   \ifte{e}{P}{Q} \sepr  \mathbf{0} 
 \end{align*}
Observe how a different font style distinguishes process variables (used in update processes)
from recursion variables. Notions of binding, $\alpha$-conversion, and substitution for recursion variables are completely standard;
 given a process $P$, we write 
  $\mathsf{frv}(P)$ and  $\mathsf{brv}(P)$ to denote its sets of  free/bound recursion variables.

 
The operational semantics for the modified language requires minor modifications.
Notions of structural congruence (Def.~\ref{d:strcong}), contexts (Def.~\ref{d:context}), and operations over contexts (Def.~\ref{d:opcontx})
are kept unchanged. The reduction semantics is the smallest relation on processes generated by 
the rules in Table~\ref{tab:semantics}, 
excepting rule $\rulename{r:ROPen}$ and adding the following additional rule:
$$
\begin{array}{ll}
 \rulename{r:Rec} &
C\{\recu\,\rv Y. P \} \pired C\{P\subst{\recu\,\rv Y. P }{\rv Y}\} 
\end{array}
$$



As for the type syntax, %We now develop required modifications in the type system.
the only addition are recursive types. 
Let us write $t, t', \ldots$ to denote recursive type variables.
The extended syntax for types is then as follows:
$$
\begin{array}{lclr}
\alpha, \beta &::=  & t & \text{type variable} \\ 
	      & \sepr &  \mu t.\alpha & \text{recursive type} \\ 	
	      & \sepr &  \cdots & \text{\{the other type constructs, as in Table \ref{tab:types} \}}	
\end{array}
$$

As customary, we adopt an \emph{equi-recursive} approach to recursive types, not distinguishing 
between $ \mu t.\alpha$ and its unfolding  $\alpha\subst{\mu t.\alpha}{t}$.
We restrict to \emph{contractive types}: a type is contractive if for each of its sub-expressions $\mu t.\mu t_1.\ldots.\mu t_n.\alpha$, the body $\alpha$ is not $t$.
Concerning typing environments,
we assume that recursion variables are included in the higher-order environment 
$\Theta$, thus extending the definition given in Table~\ref{tab:types} (lower part).
Finally, we shall require two typing rules for recursion variables and recursive calls; 
these are the first two rules in Table~\ref{tab:subt}.





\paragraph{An Example}
As a simple illustration,   consider a typical client/server scenario ($Client \para Server$) realized by the processes below:
 $$
\begin{array}{lcl}
 Server & := & \recu \, \rv Z. \nopena{a}{x}.(\rv Z \para \recu \, \rv Y.  \branch{x}{n_1{:}\inC{x}{v}.S_{\rv Y} \alte n_2{:}\close{x} } )\\
 S_{\rv Y}    & := & \nopenr{b}{z}.\outC{z}{v}.\inC{z}{r}.\close{z}.\outC{x}{r}.\rv Y \\
 Client & := & \nopenr{a}{x}. \select{x}{n_1}.\outC{x}{d_1}.\inC{x}{r}.\select{x}{n_1}.\outC{x}{d_2}.\inC{x}{r}.\select{x}{n_2}.\close{x}
\end{array}
$$
%\ref{ex:recclient}. 
We use recursion to implement (i) persistent services and (ii) services with recursive behaviors.   
Process $Server$ shows how to encode a behavior similar to $\repopen{a}{x}$: indeed once a session on $a$ is established a new copy of $Server$ is spawned. The body of the session has a recursive behavior: the client can choose between doing some computation on the server or closing the communication. If she chooses the first branch, then she sends some data to the server, the server processes them and sends back an answer $r$. At this point the client can choose again what to do: another computation or ending the session.

Processes $Server$ and $Client$ are well-typed under environments $\Gamma := v:\tau_1, r:\tau_2$ and $\Theta=\emptyset$. 
Indeed we can obtain the following type judgments:
$$
\begin{array}{ll}
 \judgebis{\env{\Gamma}{\Theta}}{Server}{\type{\emptyset}{ \quau \, a: \mu t. \&\{n_1{:}?({\capab_1}).!({\capab_2}).t, n_2{:}\epsilon \}, \quau \, b: \&\{n_1{:}!({\capab_1}).?({\capab_2}).\epsilon}}\\
 
 \judgebis{\env{\Gamma}{\Theta}}{Client}{\type{\emptyset}{ \INT}}\\
 
\end{array}
$$
where $\INT=\quau \, a: \oplus\{n_1{:}!({\capab_1}).?({\capab_2}).\oplus\{n_1{:}!({\capab_1}).?({\capab_2}). \oplus\{n_1{:}!({\capab_1}).?({\capab_2}).\epsilon, n_2{:}\epsilon \}, n_2{:}\epsilon \}, n_2{:}\epsilon \} $.
 
%\begin{table}[t!]
% 
% $$
%\begin{array}{lcl}
% Server & := & \recu \, \rv Z. \nopena{a}{x}.(\rv Z \para \recu \, \rv Y.  \branch{x}{n_1{:}\inC{x}{v}.S_{\rv Y} \alte n_2{:}\close{x} } )\\
% S_{\rv Y}    & := & \nopenr{b}{z}.\outC{z}{v}.\inC{z}{r}.\close{z}.\outC{x}{r}.\rv Y \\
% Client & := & \nopenr{a}{x}. \select{x}{n_1}.\outC{x}{d_1}.\inC{x}{r}.\select{x}{n_1}.\outC{x}{d_2}.\inC{x}{r}.\select{x}{n_2}.\close{x}
%\end{array}
%$$
% 
% 
%% $$
%% \begin{array}{lcl}
%%  Server & := & \recu \, \rv Z. \nopena{a}{x}.(\rv Z \para \outC{x}{1}.\inC{x}{y}.\recu \, \rv Y. \select{x}{y}. \branch{x}{1{:}\inC{x}{v}.S_{\rv Y}, 2{:}\close{x} } )\\
%% % S      & := & \outC{x}{1}.\inC{x}{y}.\recu \, Y. \select{x}{y}. \branch{x}{1{:}\inC{x}{v}.S_{\rv Y}, 2{:}\close{x} } \\
%%  S_{\rv Y}    & := & \nopenr{b}{z}.\outC{z}{v}.\inC{z}{r}.\close{z}.\outC{x}{r}.\inC{x}{y}.\outC{x}{y}.\rv Y \\
%%  Client & := & \nopenr{a}{x}.\inC{x}{y}.\outC{x}{1}. \recu \, \rv Y.\branch{x}{1{:}\select{x}{y}.C_{\rv Y} , 2{:}\select{x}{y}.\close{x}}\\
%% %            && \branch{x}{1{:}\select{x}{y}.C_{\rv Y} , 2{:}\select{x}{y}.\close{x}}\\
%%  C_{\rv Y}    & := & \outC{x}{d}.\inC{x}{r}.\ifte{\mathsf{ok}(r)}{\outC{x}{2}.\inC{x}{y}.Y}{\outC{x}{1}.\inC{x}{y}.\rv Y} 
%% \end{array}
%% $$
%\caption{Client/Server example}\label{ex:recclient}
%\end{table}




\subsubsection{Coinductive Subtyping and Duality}
We now introduce subtyping and duality, %essentially 
by adapting 
notions and definitions from~\cite{DBLP:journals/acta/GayH05}.
Intuitively, given session types $\alpha, \beta$, we shall say that 
$\alpha$ is a \emph{subtype} of $\beta$ %(noted $\alpha \subt \beta$) 
if %, 
%intuitively, 
any process of type $\alpha$ can safely be used in a context where a process of type $\beta$ is expected. 
More formally, let us write $\mathcal{T}$ to refer to the set of types, 
including both session types $\ST, \STT, \ldots$
and base types $\capab, \sigma, \ldots$.
We shall write 
$\ty, \tyy,  \ldots$ to range over $\mcc{T}$.
For all types, define $\unf{T}$ by recursion on the structure of $T$:
$\unf{\mu t.T} = \unf{T\subst{\mu t.T}{t}}$ and $\unf{T} = T$ otherwise.
Our definition of coinductive subtyping is given  next; it relies on 
 a subtyping relation \bsub over base types, which arises from subset relations 
(as in, e.g., $\mathsf{int} \bsub \mathsf{real}$).

%On basic types, subtyping arises from subset relations  $\mathsf{int} \subt \mathsf{real}$).
%For session types, $\subt$ is defined by the rules in Table~\ref{tab:subt}.



\begin{definition}
A relation $\mathcal{R} \subseteq \mathcal{T} \times \mathcal{T}$ is a \emph{type simulation}
if $(\ty, \tyy) \in \mathcal{R}$ implies the following conditions:
\begin{enumerate}[1.]
\item If $\unf{\ty} = \capab$ then $\unf{\tyy} = \sigma$ and $\capab \bsub \sigma$.

\item If $\unf{\ty} = \epsilon$ then $\unf{\tyy} = \epsilon$.

\item If $\unf{\ty} = ?(\ty_2).\ty_1$ then $\unf{\tyy} = ?(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $(\ty_2, \tyy_2)  \in \mcc{R}$.

\item If $\unf{\ty} = \,!(\ty_2).\ty_1$ then $\unf{\tyy} = \,!(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $(\tyy_2, \ty_2)  \in \mcc{R}$.

\item If $\unf{\ty} = ?(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\tau_i, \sigma_i) \in \mcc{R}$ and $(\ty_1, \tyy_1) \in \mcc{R}$.

\item If $\unf{\ty} = !(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = !(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\sigma_i, \tau_i) \in \mcc{R}$ and $(\ty_1, \tyy_1) \in \mcc{R}$.

\item If $\unf{\ty} = \&\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \&\{n_1:\tyy_1, \dots,  n_h:\tyy_h \}$ 
and $m \leq h$
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\item If $\unf{\ty} = \oplus\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \oplus\{n_1:\tyy_1, \dots,  n_h:\tyy_h \}$ 
and $h \leq m$
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\end{enumerate}
\end{definition}

Observe how  $\subt$ is co-variant for input prefixes and contra-variant for outputs, 
whereas it is co-variant for branching and contra-variant for choices.
We have the following definition:


\begin{definition}
The coinductive subtyping relation, denoted \csub, is defined by $T \csub S$ if and only if there exists a type simulation $\mcc{R}$
such that $(T, S) \in \mcc{R}$.
\end{definition}

Following standard arguments (as in, e.g.,~\cite{DBLP:journals/acta/GayH05}), one may show:

\begin{lemma}
\csub is a preorder.
\end{lemma}

We now move on to define duality.
It is known that 
an inductive definition of duality (cf. Def.~\ref{d:dual})
is no longer appropriate
in the presence of recursive types  (see, e.g.,~\cite{DBLP:journals/entcs/VallecilloVR03}). 
This justifies the need for a 
\emph{coinductive} notion of  duality over session types; it is defined similarly as subtyping above.



\begin{definition}
A relation $\mathcal{R} \subseteq \mathcal{T} \times \mathcal{T}$ is a \emph{duality relation}
if $(\ty, \tyy) \in \mathcal{R}$ implies the following conditions:
\begin{enumerate}[1.]
\item If $\unf{\ty} = \capab$ then $\unf{\tyy} = \sigma$ and $\tau \csub \sigma$ and  $\sigma \csub  \tau$.

\item If $\unf{\ty} = \epsilon$ then $\unf{\tyy} = \epsilon$.

\item If $\unf{\ty} = ?(\ty_2).\ty_1$ then $\unf{\tyy} = !(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $\ty_2 \csub \tyy_2$ and $\tyy_2 \csub \ty_2$.

\item If $\unf{\ty} = \,!(\ty_2).\ty_1$ then $\unf{\tyy} = \,?(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $\ty_2 \csub \tyy_2$ and $\tyy_2 \csub \ty_2$.

\item If $\unf{\ty} = ?(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\ty_1, \tyy_1) \in \mcc{R}$ and  $\tau_i \csub \sigma_i$ and  $\sigma_i \csub  \tau_i$.

\item If $\unf{\ty} = !(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\ty_1, \tyy_1) \in \mcc{R}$ and  $\tau_i \csub \sigma_i$ and  $\sigma_i \csub  \tau_i$.

\item If $\unf{\ty} = \&\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \oplus\{n_1:\tyy_1, \dots,  n_m:\tyy_m \}$ and
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\item If $\unf{\ty} = \oplus\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \&\{n_1:\tyy_1, \dots,  n_m:\tyy_m \}$ and
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\end{enumerate}

\end{definition}

We may now define:

\begin{definition}
The coinductive duality relation, denoted \cdual, is defined by $T \cdual S$ if and only if there exists a duality relation $\mcc{R}$
such that $(T, S) \in \mcc{R}$. The extension of $\csub$ to typings and interfaces, written $\ActS \csub \ActS'$ and $\INT \csub \INT'$, respectively, 
arise as expected.
\end{definition}




%\subsection{Additional typing rules}


%definire = come antisimmetria
%da aggiungere a Def. 8
%Equality between interfaces $\INT_1 = \INT_2$ iff  $\INT_1 \intpr \INT_2$ and $\INT_2 \intpr \INT_1$


\begin{table}[t!]
$$
\begin{array}{c}
\infer[\rulename{t:RVar}]{\Gamma; \Theta,\rv Y: \ActS, \INT \vdash \rv Y:\type{\ActS}{\INT}}{}
\\ \\
\infer[\rulename{t:Rec} ]{\judgebis{\env{\Gamma}{\Theta}}{\recu\,\rv Y. P}{\type{\Delta}{\INT }}} 
{\judgebis{\env{\Gamma}{\Theta,\rv Y: \type{\ActS}{\INT}}}{P}{\type{\Delta}{ \INT}} }
\\ \\
\infer[\rulename{t:Subs} ]{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS'}{\INT'}} } 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Delta}{ \INT}}& \ActS \csub \ActS' & \INT \csub \INT'}
\\
 \\
 \infer[\rulename{t:CResD}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS, [\cha^-:\ST_1], [\cha^+:\ST_2]}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, \cha^-:\ST_1, \cha^+:\ST_2 }{ \INT}} & \ST_1 \cdual \ST_2}
 \\
 \\
 \infer[\rulename{t:MonAdapt}]{\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{\mathsf{X}}}{\type{\emptyset}{ \emptyset}}}{\Theta \vdash l:\INT_1  \qquad  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT_1}}}{P}{\type{\emptyset}{ \INT_2 }}  \qquad ~\INT_1 \intpr \INT_2~}  
\end{array}
$$
\caption{Well-typed processes with recursion and subtyping: New and/or modified rules } \label{tab:subt}
\end{table}

% where the operation $\mu t(\Delta)$ stands for the concurrent promotion of all typings in $\Delta$. More formally:
% $$
% \begin{array}{lcl}
%  \mu t(\emptyset)& =& \emptyset\\
%  \mu t(\Delta, k:ST) &=& \mu t(\Delta), k:\mu t. ST\\ 
%  \mu t(\Delta, [k:ST]) &=& \mu t(\Delta), [k:\mu t. ST] \text{HMMM non sono sicura controllare!}
%  \end{array}
% $$

%We may now redefine the notion of well-typedness for the 
%the process language introduced in this section:
%
%\begin{definition}%[Well-typed process]
%A process is well-typed if it can be typed using the rules in Tables~\ref{tab:ts} and~\ref{tab:session}.
%\end{definition}

\subsubsection{Refining Interfaces via Subtyping}
In most session type disciplines, the main use of duality typically arises in the rule for channel restriction;
similarly, the main use of (coinductive) subtyping is in the subsumption rule, 
which enables us to incorporate the flexibility of subtyping in derivations, increasing typability.
 Table~\ref{tab:subt} presents these rules for our framework, denoted~\rulename{t:CResD} and~\rulename{t:Subs}, respectively.
While the former represents the key duality check performed by the typing system, the latter 
covers both typing $\ActS$ and interface $\INT$. In the following we elaborate on another consequence of adding subtyping, namely its interplay with interface ordering (cf. Def~\ref{d:intpre}).

As argued along the paper, a main contribution of this work is the extension of session type disciplines with a simple notion of \emph{interface}.
Using interfaces, we are able to give
simple and intuitive typing rules for located and update processes---see rules \rulename{t:Loc} and \rulename{t:Adapt} in Table~\ref{tab:ts}.
It is thus legitimate to investigate how to 
enhance the notion of interface and its associated definitions.
In particular, we discuss an alternative based on subtyping.
%The discussion is kept brief and informal: our aim is to illustrate how the presented framework already provides
%a basis for more sophisticated analyses---a formal treatment of these ideas is out of the scope of this paper and is left for future work.
%A straightforward enhancement concerns the typing of adaptable processes. 
Consider rule~\rulename{t:MonAdapt} in Table~\ref{tab:subt}: it is intended as 
as alternative  formulation for typing rule~\rulename{t:Adapt} in Table~\ref{tab:ts}.
Although 
rule~\rulename{t:MonAdapt} is more restrictive than~\rulename{t:Adapt} (i.e., it accepts less update processes as typable),
it captures a requirement that may be desirable in several practical settings, namely that 
the behavior after adaptation is ``at least'' the behavior offered before, possibly adding new behaviors.
Indeed, by disallowing adaptation routines that discard behavior, rule \rulename{t:MonAdapt} is suitable 
to reason about settings in which adaptation/upgrade actions need to be tightly controlled. 

In the context of more stringent typing rules such as \rulename{t:MonAdapt}, it is convenient to find ways for adding flexibility to the 
interface preorder \intpr in Def.~\ref{d:intpre}. 
As this preorder is central to our approach for disciplined runtime adaptation, 
a relaxed definition for it
may  lead to more flexible typing disciplines.
One alternative is to rely on $\csub$
%\emph{subtyping} for session types 
for such a relaxed definition:
%We briefly recall the essential features of subtyping in session types; see~\cite{DBLP:journals/acta/GayH05,DBLP:journals/fuin/VallecilloVR06} for details. 
%By relying on $\subt$, it is possible to define a more flexible preorder over interfaces:

\begin{definition}[Refined Interface Preorder] \label{d:rintpre}Given interfaces $\INT$ and $\INT'$, we write 
$\INT  \intpr_\text{sub} \INT'$ iff 
\begin{enumerate}[1.]
\item $\forall (\qual\,a{:}\ST)$ such that  
 $\#_{\INT_\qual}(\qual\,a{:}\ST) = h$  with $h > 0$,
then  one of the following holds:
\begin{enumerate}[(a)]
\item there exists $h$ distinct elements $(\qual\,a{:}\STT_i) \in \INT'_\qual$ such that 
 $\ST \csub \STT_i$ for $ i \in [1..h]$;
\item there exists $(\quau\,a{:}\STT) \in \INT'_\quau$ such that  $\ST \csub \STT$.
\end{enumerate}
\item $\forall (\quau\,a{:}\ST) \in \INT_\quau $  then $ (\quau \, a{:}\STT) \in \INT'_\quau $ and $\ST \csub \STT$, for some $\STT$.
\end{enumerate}


\end{definition}


It is immediate to see how $\intpr_\text{sub}$ improves over $\intpr$ by 
offering a more flexible and fine-grained relation over interfaces, in which subtyping replaces strict type equality.

We are now finally ready to state the notion of well-typedness that concerns the processes introduced in this section:

\begin{definition}%[Well-typed process]
A (possibly recursive) process is well-typed if it can be typed using the rules in Table~\ref{tab:ts} (excepting \rulename{t:CRes} and \rulename{t:Adapt}), Table~\ref{tab:session}, and Table~\ref{tab:subt}.
\end{definition}

%Based on this definition of well-typed process, we may now state:
%As a consequence, 
We are confident 
that our main results (Theorems~\ref{th:subred},~\ref{t:safety}, and \ref{t:consist}) 
 also hold, with little modifications, for the enhanced framework 
that results from: (a)~replacing replication with recursion, using coinductive duality, 
and (b)~incorporating subtyping, also replacing \rulename{t:Adapt} with rule \rulename{t:MonAdapt} above, using $\intpr_\text{sub}$ in place of
\intpr  
in the appropriate places in Table~\ref{tab:ts}.
%Lemma~\ref{lem:substitution}(3), and Theorem~.

%Summing up, with the modifications detail in this sub-section
%
%\begin{claim}[Subject Reduction, Recursive Processes with Subtyping]\label{th:subred-sc}
%If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced and $P \pired Q$ then 
% $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS'}{\INT'}}$, for some $\INT'$ and balanced $\ActS'$.
%\end{claim}

%\begin{proof}[Proof (Sketch)]
%TBD.
%\end{proof}




%\subsection{Example}


 
  
 \section{Related Work}\label{sec:rw}



\paragraph{Adaptation in Structured Communications}
Binary session types were first introduced in~\cite{DBLP:conf/concur/Honda93,DBLP:conf/esop/HondaVK98}.
They have been the subject of intense research in the last two decades, and 
many developments have followed.
Two notable such developments concern asynchronous communications~(see, e.g.,~\cite{DBLP:conf/forte/KouzapasYH11})
and multiparty communications~(see, e.g.,~\cite{DBLP:conf/popl/HondaYC08}, respectively).
%see~\cite{DBLP:conf/wsfm/Dezani-Ciancaglinid09} for a survey.
To the best of our knowledge, our paper~\cite{DBLP:conf/sac/GiustoP13}
was the first work \done\todo[B44.]{Fixed, pls check} to incorporate constructs for runtime adaptation (or evolvability)  into  
a session process language (either binary or multiparty). 
As stated in the Introduction, the present paper is an extended, revised version of~\cite{DBLP:conf/sac/GiustoP13}.
In particular, in this presentation the operational semantics and typing system of~\cite{DBLP:conf/sac/GiustoP13}
have been much simplified.  Following~\cite{DBLP:conf/ppdp/GarraldaCD06}, the operational semantics in~\cite{DBLP:conf/sac/GiustoP13} was
instrumented with several elements to support static analysis.
For instance, %the language in~\cite{DBLP:conf/sac/GiustoP13} features 
one such elements is
a local association between names and session types; such an association is explicitly tracked by a type annotation in prefixes for session acceptance and request. In contrast, for the sake of clarity, 
the semantics given here relies only on a simple runtime annotation for located processes; the other elements are now subsumed by the (revised) typing discipline. Also, to highlight on the simplicity and novelty of our approach, in this presentation we focus on replicated processes, rather than on recursion (the form of infinite behavior given in~\cite{DBLP:conf/sac/GiustoP13}). This is an issue orthogonal to our approach, as discussed in \S\,\ref{sec:disc}.
%\emph{We need to comment on lack of $\Delta_P$ and centralized interfaces.}\todo[B47.]{Perhaps refer here to the absence of a definition such as $\D_P$, carried over now by type judgments?}. 






After our paper~\cite{DBLP:conf/sac/GiustoP13} appeared, some works have addressed the challenging issue of analyzing runtime adaptation in scenarios of \emph{multiparty} communications, in which protocols involve more than two partners.
In such settings, there is a global specification (or \emph{choreography}) to which all interacting partners, from their local perspectives, should adhere. In the  setting of multiparty session types (see, e.g.,~\cite{DBLP:conf/popl/HondaYC08}), these two visions are described by a global type and by local types, respectively; there is a \emph{projection function} which formally relates the two.
The work~\cite{beat2013} defines both global and local languages for choreographies in which adaptation is represented by generalized forms of the adaptable processes in~\cite{BGPZFMOODS}. It is then fair to say that~\cite{beat2013} defines the foundations for extending the present approach to a multiparty setting.
The recent work~\cite{CDV14} proposes a model of self-adaptation for multiparty sessions. Key technical novelties in this approach are 
\emph{monitors} (obtained via projection of global types) and \emph{adaptation functions}. 
Monitors are coupled to processes and govern their behavior; together with global types, adaptation functions embody the runtime adaptation strategy.
An associated typed system ensures communication safety and progress. 
 \done\todo[A11.]{We have included references and comparisons to recent works on adaptations for multiparty communications.} 

\paragraph{Adaptation and Higher-Order Process Communication}
Our constructs for runtime adaptation %present in our session $\pi$-calculus 
(inherited from~\cite{BGPZFMOODS}) 
can be seen as a particular form of \emph{higher-order} communication (or \emph{process-passing}~\cite{San923}). 
In fact, as explained in \S\;\ref{ss:opsem}, our  notion of runtime adaptation formally relies on the objective \emph{movement} of an adaptation routine to a designated location. 
Session type disciplines for a higher-order $\pi$-calculus have been studied in~\cite{DBLP:conf/tlca/MostrousY07}. 
Besides data and session names, session communications in~\cite{DBLP:conf/tlca/MostrousY07}
may also involve code (i.e., process terms), leading to succinct and flexible protocol descriptions. 
%By relying on elements from the linear $\lambda$-calculus, 
The proposed typing system ensures the disciplined use of mobile code exchanged in communications; 
in particular, to avoid communication errors due to unmatched or uncompleted sessions, typing 
ensures that mobile code containing session endpoints is run exactly once. 
In contrast to the process framework in~\cite{DBLP:conf/tlca/MostrousY07}, our model has a rather implicit higher-order character, for we do not allow process communication within sessions.  
Relating our process language with the model in~\cite{DBLP:conf/tlca/MostrousY07} is a promising topic for future work. 
\done\todo[A12.]{We have contrasted our approach to session types for higher-order pi~\cite{DBLP:conf/tlca/MostrousY07}} %d, structured behavior. %determined by the runtime behavior of the system.
Our constructs for runtime adaptation are also related to \emph{passivation} operators found in 
higher-order process calculi (see, e.g.,~\cite{LengletSS11}). There are significant differences between adaptable processes and passivation; 
in particular, adaptable processes distinguish from calculi 
with passivation in that process update   is defined without assuming constructs for higher-order process communication.
See~\cite[\S9.1]{BGPZFMOODS} for a detailed comparison between adaptable processes and passivation.

As already discussed, % along the paper, 
our approach has been influenced by~\cite{DBLP:conf/ppdp/GarraldaCD06} and our previous work~\cite{BGPZFMOODS}. 
Nevertheless, 
there are several major differences between 
our framework and those works. %~\cite{DBLP:conf/ppdp/GarraldaCD06}.
(i)~Unlike the system in~\cite{DBLP:conf/ppdp/GarraldaCD06}, our framework supports channel passing (delegation).
As delegation is already useful to 
represent forms of dynamic reconfiguration, its interplay with update actions is very appealing (cf. the example in \S\,\ref{ss:behdist}).
%\jp{this is no longer useful} 
(ii)~We have extended typing
judgments in~\cite{DBLP:conf/ppdp/GarraldaCD06} with \emph{interfaces} $\INT$, which are % of processes.
central to characterize located processes which can be safely updated. 
%with its two zones, $\Delta_l$ and $\Delta_u$. % and by the necessity of distinguishing between linear and unrestricted actions.
%Another distinctive feature of our approach is the treatment in the typing of the restriction operator. 
%In our setting, communication can happen at any level in the hierarchy of adaptable processes; hence, 
%in order to correctly type the number of active sessions (which, as discussed, is central to enable evolvability steps), the information on used session (e.g. $c:\bot$) cannot be hidden.
%Differences with respect to our previous work~\cite{BGPZFMOODS} are also important.
(iii)~While in~\cite{BGPZFMOODS} adaptable processes are defined for a %(restriction-free) 
fragment of CCS, 
here we consider them within a typed $\pi$-calculus.
(iv)~Adaptation steps in~\cite{BGPZFMOODS} are completely unrestricted. 
%i.e., an update will occur as soon as a located process and an update prefix are able to interact. 
Here we have considered annotated versions of the constructs in~\cite{BGPZFMOODS}:
% Here we have added two elements 
%which serve as a guard for enabling evolvability steps: the number of open sessions in the located processes
%and the interface $\Delta$, present both in the located process and in interacting update processes.
%we think that %our framework enhances the main insights of~\cite{BGPZFMOODS} by 
%they allow to represent evolvable, concurrent systems in a more realistic way, as
%taking the idea of adaptable process to a much more realistic setting, in which 
they offer a more realistic account of update actions, as they are supported 
by runtime conditions based on session types.


\paragraph{Runtime Adaptation} Recently, there has been an increasing interest in %proper definitions of
the specification and verification of autonomic and (self-)adaptive computer systems. 
As a result, several definitions and characterizations of (self-)adaptation have been put forward: 
they reflect the different perspectives and approaches of the several research communities  interested in this class of systems. 
In the Introduction, we have stated our vision of runtime adaptation for communication-based systems. Here we then limit to remark that this vision is well-aligned with the conceptual definition of adaptation recently given in~\cite{DBLP:conf/fase/BruniCGLV12}: ``Given a component with a distinguished collection of control data, adaptation is the runtime modification of such control data.'' 
%As remarked in~\cite{BGPZFMOODS}, 
In the case 
of the calculus of adaptable processes, 
\emph{control data} refers to the located processes in which   behavior can be structured.
The same observation applies for the session calculus considered here, noticing that our framework precisely defines the runtime conditions in which adaptation may consistently occur.


\paragraph{Adaptation vs Exceptions and Compensations}

From a high-level perspective, our typed framework can be related to formal models for service-oriented systems
with constructs such as exceptions and compensations (e.g.,~\cite{DBLP:conf/concur/CarboneHY08,DBLP:books/sp/sensoria2011/FerreiraLRVZ11}). 
In particular,~\cite{DBLP:conf/concur/CarboneHY08} develops a typeful approach for \emph{interactional exceptions}
in asynchronous, binary session types. There, services define a default process and an exception handler, and may be influenced by 
a $\mathtt{throw}$ construct used to throw exceptions;
the associated type system ensures consistent dynamic escaping from possibly nested exception scopes in a concerted way.
We find conceptual differences between 
our intended notion of runtime adaptation (described in the Introduction) and
mechanisms for 
exceptions and compensations.
In our view, such mechanisms 
are concerned only with a particular instance of adaptation/evolvabilty scenarios. 
This way, forms of exceptions (e.g., the one in~\cite{DBLP:conf/concur/CarboneHY08}) should typically handle \emph{internal events}
which  arise during the program's execution and may affect its flow of control. 

Similar in several respects to exceptions, constructs for compensations are usually conceived for 
handling events which are often exceptional \emph{and} catastrophic, such as runtime errors.
This is in contrast with runtime adaptation in modern distributed systems, which 
relies on \emph{external} mechanisms tailored to 
handle general exceptional events, not necessarily catastrophic.
%A familiar example of such events are program upgrades, whose execution can be anticipated and incorporated into the program's code for eventual execution. 
As an example, consider elasticity in cloud-based applications, 
i.e., the ability such applications have to acquire/release computing resources based on user demand.
%depending on user activity, they determine how/when to .
%that in peaks of high activity additional computing resources must be acquired.
Although elasticity triggers 
%Such peaks, while triggering 
system adaptation, % of the system architecture, 
it does not represent a catastrophic event; rather, 
it represents an acceptable (yet hard to predict) state of the system.
Due to this conceptual difference, 
we do not have a clear perspective as to how 
formally relate our approach with 
known models of exceptions/compensations.

%\todo{
Somewhat related to our approach is the work~\cite{DBLP:conf/aplas/AndersonR12}, 
where dynamic runtime update for message passing programs with queues is studied, 
and 
a form of consistency for updates over threads is ensured using 
multiparty session types.
As in our setting,
the notion of update in~\cite{DBLP:conf/aplas/AndersonR12} does not require
  a complete system shutdown, while ensuring that the state of the program remains consistent. 
  However, there are significant 
  conceptual and technical differences. % between our work and~\cite{DBLP:conf/aplas/AndersonR12}. 
First, unlike our approach, in~\cite{DBLP:conf/aplas/AndersonR12} update actions (or adaptation routines)
are defined independently and externally from the program's syntax. 
Second,  here we have considered synchronous communication, 
whereas in~\cite{DBLP:conf/aplas/AndersonR12} an asynchronous thread model with queues is used.
Third, while we have analyzed updates for a language endowed with  binary session types, 
in~\cite{DBLP:conf/aplas/AndersonR12} the need for reaching agreements on multiple threads leads to the use of multiparty session 
types to ensure consistent updates.




\paragraph{Adaptation in Other Settings}
It is instructive to note that approaches similar to ours can also be found in the sequential formalisms for reasoning at lower levels of abstraction. For instance, in~\cite{DBLP:journals/toplas/StoyleHBSN07} the authors introduce dynamic updates to C-like languages, with a focus on runtime update of functions and type declarations. 
They show that dynamic updates are type-safe (consistent) as it cannot happen that different parts of the program expect
different representations of a type. Although the aim is similar, 
it is difficult to establish more precise comparisons, for our interest is in high-level reasoning for communicating programs with precise protocol descriptions.
%clearly, the setting is completely different as moving from a sequential to a concurrent scenario changes considerably the techniques and the problems to be solved.
%}
 In~\cite{DBLP:conf/amast/BrogiCP04} the authors also investigate behavioral types for adaptation, but 
 in the different setting of component-based systems.
Their notion of runtime adaptation %  \todo{different how?} 
relies on a notion of interface which describes the 
behavior of each component. These interfaces are to be used to implement inter-component communication. 
As it could that composition might not work because of  interface mismatching, 
the authors introduce the notion of  \emph{adaptors}, i.e., a software piece that  acts as mediator between two communicating components. It is interesting to notice that a similar mediator behavior could be implemented in our setting, as described in \S\,\ref{ss:behdist}.
%}



%\newpage
%\jp{Other related stuff: \cite{DBLP:conf/aplas/AndersonR12}, possibly also related: \cite{DBLP:conf/isola/LaneseM10,Ivan-Adaptive_C:2013}}
\section{Concluding Remarks}\label{sec:conc}
A main motivation for our work is the observation that while 
paradigms such as service-oriented computing are increasingly popular among practitioners, % software architects and programmers,
formal  models  based on them---such
%core programming calculi based on them---such
as analysis techniques based on session types---fail to capture  
distinctive aspects of such par\-a\-digms.
Here we have  addressed, for the first time, one of such aspects\done\todo[B46.]{We do not like the singular form.}, namely \emph{runtime adaptation}. 
In our view, it
%Here we have addressed one such aspects, runtime adaptation, 
represents an increasingly important concern when analyzing the behavior of communicating systems in 
%, which is intimately related to the fact that service oriented systemsare increasingly being deployed in very highly 
open, context-aware computing infrastructures.

%In this paper w
We have proposed a  framework for
%alternative \todo{approach?} for 
%specifying and 
reasoning about  runtime ad\-ap\-ta\-tion in the context of structured communications
described by session types.
Amalgamating a static analysis technique for correct communications (session types) 
with a novel, inherently dynamic form of interaction (runtime adaptation actions on located processes) is challenging, for 
it requires balancing two different (but equally important) concerns in modern interacting systems. 
In our approach, we %investigated 
are concerned with\done\todo[B45.]{Fixed, pls check}
a session type discipline for an
extended $\pi$-calculus, in which channel mobility (delegation) is enhanced 
with the possibility of performing sophisticated update actions on located processes.
We purposefully aimed at integrating existing, well-studied lines of work: we expect this to be beneficial  for the 
enhancement of other known session type disciplines with adaptation concerns. 
In particular, we built upon our previous work on  
process abstractions for evolvability~\cite{BGPZFMOODS} and
on session types for mobile calculi~\cite{DBLP:conf/ppdp/GarraldaCD06}, relying also on 
a modern account of binary session types~\cite{DBLP:journals/entcs/YoshidaV07}.
In addition to runtime correctness (safety), our typing discipline
ensures consistency: this guarantees that communication behavior (as declared by types) is not disrupted by potential update actions.

%It is aimed at supporting the analysis of service-oriented applications/systems.

There are several avenues for future developments. In ongoing work, we are exploring the use of a 
\emph{typecase} operator (similar to the one proposed in~\cite{DBLP:conf/forte/KouzapasYH11}) to support the runtime adaptation of processes with running sessions. As detailed in \S\,\ref{sec:disc}, this is a challenging issue, for it requires having a uniform treatment of process behavior and the current state of sessions. 
Also, we intend to continue the study of runtime adaptation in a multiparty setting, developing further the approach recently introduced in~\cite{beat2013}.
Furthermore, we plan to investigate 
the interplay of runtime adaptation with
issues such as deadlock-freedom/progress~\cite{DBLP:conf/tgc/Dezani-CiancaglinidY07,DBLP:journals/corr/abs-1010-5566} and  properties related to security, such as access control and information flow~\cite{DBLP:conf/concur/CapecchiCDR10}. 
%In fact, a formal connection between runtime adaptation and security remains to be explored, for runtime errors and security leaks could be p
%which are also important and challenging. %---we plan to look into these in the future. 
%Nevertheless, we believe 
%our work already contributes to the understanding of 
%%that a major contribution of our paper %is novel, as it  is to address 
%issues which, to our knowledge, have not yet  been explored in the realm of 
%session-typed %interacting 
%processes. 




%Our proposal, we believe, combines the most interesting aspects of these previous works in the context of the unexplored setting of evolvable session-typed processes. 
%\newpage
%
%As future work, we plan to investigate stronger notions of correctness for our adaptable, session-typed processes, in particular deadlock-freedom.
%Also, following~\cite{DBLP:journals/acta/GayH05} and the discussion in Sect.\ref{sec:int}, 
%we would like to integrate subtyping into our type system,
%and to obtain algorithmic characterizations
%of notions such as type duality and interface compatibility. 
%This work is an initial 
%step towards a theory of interaction
%in which processes---endowed with behavioral disciplines expressed as types---may dynamically evolve at runtime. 




% . \\%ways of enabling evolvability steps. \\
%-As future work, we plan to investigate stronger notions of correctness for adaptable, session-typed processes, and 
%to develop a formal treatment of subtyping and interface compatibility, along the discussion in Sect.\ref{sec:int}. \\%ways of enabling evolvability steps. \\



\paragraph{Acknowledgments}
%We thank 
%Ant\'{o}nio Ravara,
%Fabrizio Montesi, 
% and
%the SAC'13 and PLACES'13 
We thank the anonymous reviewers for their  detailed remarks. 
This work was 
partially 
supported by the French project
%ANR-11-INSE-0007- REVER and
ANR BLAN 0307 01 - SYNBIOTIC, as well as 
by the 
%Funda\c{c}\~{a}o para a Ci\^{e}ncia e a Tecnologia (
Portuguese Foundation for Science and Technology (FCT) %) 
%through the Carnegie Mellon Portugal Program (grant INTERFACES NGN-44 / 2009) and 
grants  SFRH\;/\;BPD\;/\;84067\;/\;2012
and CITI.
 
%We thank the anonymous reviewers for their useful comments.



 
 
 \todos
% 

{\small
\bibliographystyle{abbrv}
\bibliography{referen}
}

\appendix
\section{Auxiliary Definitions}
\subsection{Cardinality of Typings\label{ap:count}}
\begin{definition}
Let $\ActS$ be a typing, as in Table~\ref{tab:types}. The cardinality of $\ActS$, denoted $|\ActS|$, is inductively defined as follows:
\begin{align*}
|\emptyset| & = 0 \\
|\ActS', k:\ST| & = 1 + |\ActS'| \\
|\ActS', [k:\ST]| & = 1 + |\ActS'| \\
\end{align*}
\end{definition}


\section{Proofs from \S\,\ref{sec:res}}

\subsection{Proof of Theorem~\ref{th:congr}\label{app:congr}}
We repeat the statement given in Page~\pageref{th:congr} and give its proof.

\begin{theorem}[Subject Congruence] 
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ and $P \equiv Q$ then $\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}$.
\end{theorem}
\begin{proof}
By induction on the derivation of $P \equiv Q$, with a case analysis on the last applied rule.

%\begin{description}
\paragraph{\bf Case $\restr{\cha}{ ( \compo{l}{h}{P})  } \equiv   \compo{l}{h}{ \restr{\cha}{P}  }$} \quad \\
We examine the left to right direction:
we show that if 
$\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{ ( \compo{l}{h}{P} ) }}{\type{\ActS}{\INT}}$ 
then 
$\judgebis{\env{\Gamma}{\Theta}}{  \compo{l}{h}{\restr{\cha}{P}  }}{\type{\ActS}{\INT}}$.
Since $\restr{\cha}{  (\compo{l}{h}{P} ) }$ is well-typed, 
by inversion on rules \rulename{t:Loc} and \rulename{t:CRes}, 
for some $\ST, \Delta'$
we have:
$$
\cfrac{
\begin{array}{c}
\Theta \vdash l:\INT' \\
\INT \sqsubseteq \INT'
\end{array}
\quad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS', \cha^-:\ST, \cha^+:\overline{\ST}}{\INT} } \quad
 h = | \ActS', \cha^-:\ST, \cha^+:\overline{\ST} |  
}{\cfrac{\judgebis{\env{\Gamma}{\Theta}}{\compo{l}{h}{P} }{ \type{\ActS', \cha^-:\ST, \cha^+:\overline{\ST}}{\INT}}} {\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{(\compo{l}{h}{P})}}{\type{\ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT }}}}
$$ 
%\jp{perhaps this is redundant:} 
Hence $ \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS', \cha^-:\ST, \cha^+:\overline{\ST}}{\INT}}$, 
where $\ActS = \ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]$.
Now, starting from $P$, and by applying first rule  \rulename{t:CRes} and then rule  \rulename{Loc} we obtain: 
$$
\cfrac
{
\cfrac{
 \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS', \cha^-:\ST, \cha^+:\overline{\ST}}{\INT} } 
}
{ 
\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT}}}
\ 
\begin{array}{c}
\Theta \vdash l:\INT' \qquad \INT \sqsubseteq \INT' \\
 h = | \ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]| 
\end{array}
}
{\judgebis{\env{\Gamma}{\Theta}}{\compo{l}{h}{\restr{\cha}{P}} }{ \type{\ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]}{\INT}}}
$$
Observe that 
$h = | \ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]| =  | \ActS', \cha^-:\ST, \cha^+:\overline{\ST}|$---bracketing does not influence $h$, i.e.,
The reasoning for the right to left direction is analogous and omitted.


\paragraph{\bf Case $P \para \nil  \equiv P $} \quad \\ 
We examine only the left to right direction; the converse direction is similar. 
We then show that if  $\judgebis{\env{\Gamma}{\Theta}}{P \para \nil }{\type{\ActS}{\INT}}$
then  $\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{\INT}}$.
 By inversion on rule \rulename{t:Par}  there exist $\Delta_1, \INT_1$ such that $$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{\INT_1}} \text{ and }  \judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}$$
with  $\ActS= \ActS_1 \cup \emptyset = \ActS_1$ and $\INT = \INT_1 \uplus \emptyset = \INT_1$ and so the thesis follows.




\paragraph{\bf Case $\restr{\cha}{P} \para Q \equiv \restr{\cha}{(P \para Q)}$ with $\cha \notin \mathsf{fc}(Q) $} \quad \\
We examine only the right to left direction; the other direction is analogous.
We show that if 
$\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{(P \para Q)}}{\type{\ActS}{\INT}}$ (with $\cha \notin \mathsf{fc}(Q)$) then 
also 
$\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{P \para Q}}{\type{\ActS}{\INT}}$.
By inversion on rules 
\rulename{t:CRes} and \rulename{t:Par}
we have:
$$
\cfrac{
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1,  \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT_1}} \qquad
 \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
 \qquad
 \INT = \INT_1 \addelta \INT_2}
{ \cfrac{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2, \cha^-:\ST, \cha^+:\overline{\ST} }{\INT'}}}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{(P\para Q)}}{\type{\ActS_1 \cup \ActS_2, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT }}}}
$$
where $\ActS = \ActS_1 \cup \ActS_2, [\cha^-:\ST], [\cha^+:\overline{\ST}]$.
Observe how in the inversion of rule \rulename{t:Par} we
may combine assumption 
$\cha \notin \mathsf{fc}(Q)$ with $\alpha$-conversion to infer 
$\cha \notin \mathsf{fc}(Q) \cup \mathsf{bc}(Q)$. We may then use Lemma \ref{lem:channel}  to infer 
$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1,  \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT_1}}$ and $ \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}$. Now, % and we can construct the following derivation tree
using first rule  \rulename{t:CRes} and then rule  \rulename{t:Par} we have:
 $$
\cfrac{ 
\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1,  \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT_1}}}
{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS_1, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT_1 }}}
\quad 
\begin{array}{c}
\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
\\
 \INT = \INT_1 \addelta \INT_2
\end{array}
 } 
{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}\para Q}{\type{\ActS_1 \cup \ActS_2, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT }}}
$$
%The converse is similar.

\paragraph{\bf Case $\restr{\cha}{ \nil  } \equiv \nil$ } \quad \\ This case is easily proven by appealing to rule \rulename{t:Weak}.


\paragraph{\bf Cases $P \para Q  \equiv Q \para P$ and $(P \para Q )\para R \equiv P \para (Q \para R)$} \quad \\ 
In both cases, the proof  follows by commutativity and associativity of $\cup$ and $\uplus$ (cf. Def.~\ref{d:interf}).

\paragraph{\bf Case $\restr{\cha}{\restr{\cha'}{P}} \equiv \restr{\cha'}{\restr{\cha}{P}}$} \quad \\  This case is similar to previous ones.
%\end{description}
\end{proof}


\subsection{Proof of Theorem~\ref{th:subred}\label{app:subred}}

The proof of Theorem~\ref{th:subred} relies on the following lemma that  allows to reverse typing rules. 
\begin{lemma}[Inversion Lemma] \label{lem:types} \quad \\
\begin{description}

 \item [\rulename{t:Accept}:] \label{types8} if $\judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P}{ \type{\ActS}{\INT \uplus a:\alpha_\qual}}$ then $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\alpha}{ \INT}}$;
  
 \item [\rulename{t:RepAccept}:] \label{typesrepa} if $\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P}{ \type{\ActS}{\INT \uplus a:\alpha_\quau}}$ then there exists $\INT'$ such that  $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\alpha}{ \INT'}}$;

 \item [\rulename{t:Request}:] \label{typesreq} if $\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{x}.P}{ \type{\ActS}{\INT \uplus a:\overline{\alpha}_\qual}}$ then $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\overline{\alpha}}{ \INT}}$;

 \item [\rulename{t:Close}:] \label{types9} if $\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS,k:\epsilon}{ \INT}}$ then  $\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}}$;
   
 \item [\rulename{t:Loc}:]\label{types6} if $\judgebis{\env{\Gamma}{\Theta}}{\component{l}{h}{\INT}{P} }{ \type{\ActS}{\INT}}$ then $\Theta \vdash l:\INT' $, $\judgement{\Gamma}{\Theta}{P}{\ActS}{\INT}$, $h = |\ActS|$ and $\INT \intpr \INT'$;
 
 \item [\rulename{t:Adapt}:] \label{types7} if $\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{X}}{\type{\emptyset}{ \emptyset}}$ then  $\Theta \vdash l:\INT $ and there exists $\INT'$ such that $\judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT}}}{ P}{\type{\emptyset}{ \INT' }}$;
 
 \item [\rulename{t:CRes}:] \label{types10} if $\judgement{\Gamma}{\Theta}{\restr{\cha}{P}}{\ActS, [\cha^-:\alpha], [\cha^+:\overline{\alpha}]}{\INT}$  then $\judgement{\Gamma}{\Theta}{P}{\ActS,\cha^-:\alpha, \cha^+:\overline{\alpha}}{\INT}$;
 
 \item [\rulename{t:Par}:]\label{types1} if $\judgement{\Gamma}{\Theta}{P \para  Q}{\ActS}{\INT}$ then there exists $\ActS_1, \ActS_2, \INT_1, \INT_2$  such that $\judgement{\Gamma}{\Theta}{P}{\ActS_1}{\INT_1}$,  $\judgement{\Gamma}{\Theta}{Q}{\ActS_2}{\INT_2}$, $\ActS= \ActS_1 \cup  \ActS_2$ and $\INT = \INT_1 \uplus \INT_2$;
 
 \item [\rulename{t:Thr}:]\label{typesdelout} if $\judgement{\Gamma}{\Theta}{\throw{k}{k'}.P}{\ActS, k:!(\alpha).\beta, k':\alpha}{\INT}$ then  $\judgement{\Gamma}{\Theta}{P}{\ActS, k:\beta}{\INT}$;
 
 
 \item [\rulename{t:Cat}:]\label{typesdelin} if $\judgement{\Gamma}{\Theta}{\catch{k}{x}.P}{\ActS,k?(\alpha).\beta}{\INT}$ then $\judgement{\Gamma}{\Theta}{P}{\ActS, k:\beta, x:\alpha}{\INT}$;
 
 
 \item [\rulename{t:In}:] \label{types2} if $\judgement{\Gamma}{\Theta}{\inC{k}{\widetilde{x}}.P}{\ActS,k:?(\widetilde{\tau}).\alpha}{\INT}$  then $\judgement{\Gamma, \widetilde{x}:\tilde{\tau}}{\Theta}{P}{\ActS, k:\alpha}{\INT}$ and $\Gamma \vdash \widetilde{e}:\widetilde{\tau}$;
 
 \item [\rulename{t:Out}:]\label{types3} if $\judgement{\Gamma}{\Theta}{\outC{k}{\widetilde{e}}.P}{\ActS,k:!(\widetilde{\tau}).\alpha}{\INT}$ then $\judgement{\Gamma}{\Theta}{P}{\ActS, k:!(\widetilde{\tau}).\alpha}{\INT}$;

 \item [\rulename{t:If}:] \label{types5} if $\judgement{\Gamma}{\Theta}{\ifte{e}{P}{Q}}{\ActS}{\INT}$ then $\judgement{\Gamma}{\Theta}{P}{\ActS}{\INT}$,  $\judgement{\Gamma}{\Theta}{Q}{\ActS}{\INT}$ and $\Gamma \vdash e:\mathsf{bool} $;
 
 \item [\rulename{t:Bra}:] \label{types12} if $\judgebis{\env{\Gamma}{\Theta}}{\branch{k}{n_1:P_1 \alte \dots \alte n_m:P_m}}{\type{ \ActS, k:\&\{n_1:\alpha_1, \dots , n_m:\alpha_m \}}{ \INT}}$ then there exists $\INT_1, \dots, \INT_m$ such that for all $i\in [1..m]$, $\judgebis{\env{\Gamma}{\Theta}}{P_i}{\type{\ActS, k:\alpha_i}{ \INT_i}}$;
 
 \item [\rulename{t:Sel}:]\label{types13} if $\judgebis{\env{\Gamma}{\Theta}}{\select{k}{n_i}.P}{\type{\ActS, k:\oplus\{n_1:\alpha_1, \dots, n_m:\alpha_m\}}{\INT}}$ then $i\in [1..m]$ and $\judgebis{ \env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\alpha_i}{ \INT}}$.
\end{description}
\end{lemma}
\begin{proof}
Follows directly from the definition of typing system.
\end{proof}




We repeat the statement in Page~\pageref{th:subred} and present its proof.

\begin{theorem}[Subject Reduction]
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced and $P \pired Q$ then 
 $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS'}{\INT'}}$, for some $\INT'$ and balanced $\ActS'$.
\end{theorem}


\begin{proof}
%The proof proceeds by 
By induction on the last rule applied in the reduction. %See~\ref{app:subred} for details. 
We assume that $\til{e} \downarrow \til{c}$ is a type preserving operation, for every $\til{e}$.
%\begin{description}
\paragraph{\bf Case \rulename{r:Open}} From Table~\ref{tab:semantics} we have:
\begin{multline*} 
E\big\{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}\big\} \pired  \\
E^{++}_{} \big\{\restr{\cha}{\big({C^{+}_{}\{P_1\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\} }\big)\big\} } 
\end{multline*}
By assumption  $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_{2}\}\big\} }{\type{\ActS}{\INT}}$
with balanced $\ActS$.
Then, by %the following derivation tree using Lemma \ref{lem:context} ($\Leftarrow$) three times,  and  
inversion on typing, using rules \rulename{t:Fill}, \rulename{t:Accept}, \rulename{t:Request}, and \rulename{t:Par} we infer
there exist $\ActS', \INT'$ such that
{%\small
\begin{equation}\label{eq:wholeopen}
\infer
{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_{2}\}\big\}}{\type{\ActS}{\INT }}}
{
\judgebis{\bullet_{\jug_0} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{ \INT }}   & 	\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_{2}\}}{\type{\ActS'}{\INT'}}}
{    \eqref{eq:typeaccept} & \eqref{eq:typerequest}
}}
\end{equation}
}
where
$ \INT' = (\INT'_1 \addelta a:\ST_\qual) \addelta (\INT'_2\addelta a:\overline{\ST}_\qual )$
%$\{ a:\ST_\qual \addelta a:\overline{\ST}_\qual \} \subseteq \INT$, 
and
\begin{equation}
\jug_0 = \Gamma; \Theta \vdash \type{\ActS'}{\INT'} \label{eq:srjug0}
\end{equation}
%Moreover,
By Lemma~\ref{lem:context},  
$\ActS' \subseteq \ActS$ and $\INT' \intpr \INT$.
Then, letting $\ActS' = \ActS'_1 \cup \ActS'_2$, 
subtree \eqref{eq:typeaccept} is as follows: %\todo[JP:]{We should explain why $\ActS$ is different from $\ActS'$}:
\begin{equation}\label{eq:typeaccept}
\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\nopena{a}{x}.P_1\}}{\type{\ActS_1'}{ \INT_1'\addelta a:\ST_\qual }}}		  
    { 
 	\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1}{ \INT'_1\addelta a:\ST_\qual}} & \infer{\judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P_1}{\type{\ActS_1}{ \INT_1\addelta a:\ST_\qual  }}}
  {\Gamma \vdash a: \langle \ST_\qual , \overline{\ST}_\qual \rangle &
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1, x:\ST}{\INT_1}} }}
\end{equation}
with 
\begin{equation}
\jug_1 = \Gamma; \Theta \vdash \type{\ActS_1}{\INT_1 \addelta a:\ST_\qual} \label{eq:srjug1}
\end{equation}
Then, subtree~\eqref{eq:typerequest} is as follows:
\begin{equation}\label{eq:typerequest}
\infer{\judgebis{\env{\Gamma}{\Theta}}{D\{\nopenr{a}{y}.P_{2} \}}{ \type{\ActS'_2}{ \INT'_2\addelta a:\overline{\ST}_\qual }}}
	{\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2}{ \INT'_2\addelta a:\overline{\ST}_\qual}} &  \infer{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{y}.P_{2}}{ \type{\ActS_2}{ \INT_2\addelta a:\overline{\ST}_\qual }}}
	{\Gamma \vdash a: \langle \ST_\qual , \overline{\ST}_\qual \rangle &
\judgebis{\env{\Gamma}{\Theta}}{P_{2}}{\type{\ActS_2, y:\overline{\ST}}{\INT_2}}}
}
 \end{equation}
 with 
 \begin{equation}
 \jug_2 = \Gamma; \Theta \vdash \type{\ActS_2}{\INT_2 \addelta a:\overline{\ST}_\qual} \label{eq:srjug2}
 \end{equation}
By Lemma~\ref{lem:context} 
% ($\Leftarrow$) 
%there exist $\ActS_1, \ActS_2$ such that 
we have that 
$\ActS_1 \subseteq \ActS_1'$ and $\ActS_2 \subseteq \ActS_2'$. We also infer $\INT_1 \intpr \INT_1'$, $\INT_2 \intpr \INT_2'$, and $\INT' \intpr \INT$. 
 Now, using Lemma~\ref{lem:substitution}(\ref{subchavar}) on judgments for $P_1$ and $P_2$, we obtain:
 \begin{enumerate}[(a)]
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_1\sub{\cha^+}{x}}{ \type{\ActS_1, \cha^+:\ST}{\INT_1}}$.
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}$.
 \end{enumerate}
%By using Lemma \ref{lem:context}($\Rightarrow$)  and typing rules \rulename{t:Par} and \rulename{t:CRes} 
We now describe how to obtain appropriately typed contexts $C^+, D^+$, and $E^{++}$ based on the information inferred up to here
on contexts $C, D$, and $E$.
%We give details for the case of $C^+$; cases for $D^+$ and $E^{++}$ follow analogously. 
We first describe the case of $C^+$.
From \eqref{eq:typeaccept} above we obtained
$\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1}{ \INT'_1 \addelta a:\ST_{\qual}}}$
with $\jug_1$ as in \eqref{eq:srjug1}.
Then, using Lemma~\ref{l:ctxop}(1), we infer
$\judgebis{\bullet_{\jug_3}; \env{\Gamma}{\Theta}}{C^+}{\type{\ActS'_1, \cha^+:\ST}{ \INT'_1}}$
with 
 \begin{equation}
 \jug_3 =  \Gamma; \Theta \vdash \type{\ActS_1, \cha^+:\ST}{\INT_1} \label{eq:srjug3}
 \end{equation}
We may now reconstruct the derivation given in \eqref{eq:typeaccept}:
%$$R \triangleq {{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\} }},$$
\begin{equation}\label{eq:typeacceptsub}
\infer{\judgebis{\env{\Gamma}{\Theta}}{C^{+}\{P_{1}\sub{\cha^+}{x}\}}{\type{\ActS_1', \cha^+:\ST}{ \INT_1' }}}		  
    { \judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{C^+}{\type{\ActS'_1, \cha^+:\ST\,}{ \INT'_1}} &  
    	\judgebis{\env{\Gamma}{ \Theta}}{P_{1}\sub{\cha^+}{x}}{ \type{\ActS_1, \cha^+:\ST}{\INT_1}}}
\end{equation}
For $D^+$, we proceed analogously from \eqref{eq:typerequest} and infer:
\begin{equation}\label{eq:typerequestsub}
 \infer{\judgebis{\env{\Gamma}{\Theta}}{D^{+}\{P_{2}\sub{\cha^-}{y}\}}{\type{\ActS'_2,\cha^- :\overline{\ST } }{\INT'_2}}}
	{\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D^+}{\type{\ActS'_2, \cha^-:\overline{\ST}}{ \INT'_2}} & \judgebis{\env{\Gamma}{ \Theta}}{P_{2}\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}}
\end{equation}
with 
 \begin{equation}
 \jug_4 =  \Gamma; \Theta \vdash \type{\ActS_2, \cha^-:\overline{\ST}}{\INT_2} \label{eq:srjug4}
 \end{equation}
To infer the type of $E^{++}$ we proceed as before using twice Lemma~\ref{l:ctxop}(1), combined with~\eqref{eq:srjug0}.
We may finally derive the type for the result of the reduction: using rules \rulename{t:Par}, \rulename{t:CRes}, and \rulename{t:Fill} we obtain:
$$
\infer
{\judgebis{\env{\Gamma}{\Theta}}{E^{++}_{} \big\{\restr{\cha}{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\}} \big\} }{\type{\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT''}}}
{\eqref{eq:last}   &
	\infer{\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\}}}{\type{\ActS', [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT_1' \addelta \INT_2'}}}
{\infer{\judgebis{\env{\Gamma}{\Theta}}{{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\} }}{\type{\ActS', \cha^+:\ST, \cha^-:\overline{\ST} }{ \INT_1' \addelta \INT_2'}}}{
\eqref{eq:typeacceptsub}
%
&
%
	\eqref{eq:typerequestsub}
}
}}
$$
with 
 \begin{equation}\label{eq:last}
\judgebis{\bullet_{\jug_5} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]}{ \INT'' }}
 \end{equation}
and 
$$
 \jug_5 =  \Gamma; \Theta \vdash \type{\ActS', \cha^+:\ST, \cha^-:\overline{\ST} }{ \INT_1' \addelta \INT_2'}
$$

Notice that by Lemma \ref{lem:context}, we have $\INT'' \intpr \INT_1' \cup \INT_2'$.
Also, observe that by assumption $\ActS$ is balanced; therefore, 
by Def.~\ref{d:balanced}
the resulting typing $\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]$ is balanced too.
This concludes this case. 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\paragraph{\bf Case \rulename{r:ROpen}} From Table~\ref{tab:semantics} we have: 
\begin{multline*}
          E\big\{C\{\repopen{a}{x}.P_1\}  \para  D\{\nopenr{a}{y}.P_2\} \big\}  \pired  \\
E^{++}_{}\big\{\restr{\cha}{\big({C^{+}_{}\{P_1\sub{\cha^+}{x}  \para \repopen{a}{x}.P_1 \}  \para  D^{+}_{}\{P_2\sub{\cha^-}{y}\} }\big)}\big\}  
         \end{multline*}

\noindent By assumption $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\repopen{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}\big\} }{\type{\ActS}{\INT}}$, with balanced $\ActS$.  
Then, by inversion on typing, using rules
%is obtained by the following derivation tree using Lemma \ref{lem:context}($\Leftarrow$) three times and inversion on  rules 
\rulename{t:Fill}, 
\rulename{t:RepAccept}, \rulename{t:Request}, and \rulename{t:Par}, we infer there exist $\ActS'$, $\INT'$ such that:
$$
\infer
{ \judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\repopen{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}\big\}}{\type{\ActS}{\INT}}}
{ \judgebis{\bullet_{\jug_0} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{ \INT }}  & \infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\repopen{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}}{\type{\ActS'}{\INT'}}}
{
\eqref{eq:bangaccept}
%
&
%
\eqref{eq:bangrequest}
}}
$$
where
$ \INT' = (\INT'_1 \addelta a:\ST_\quau) \addelta (\INT'_2\addelta a:\overline{\ST}_\qual )$
%$\{ a:\ST_\qual \addelta a:\overline{\ST}_\qual \} \subseteq \INT$, 
and
\begin{equation}
\jug_0 = \Gamma; \Theta \vdash \type{\ActS'}{\INT'} \label{eq:srjugro0}
\end{equation}
By Lemma~\ref{lem:context},  
$\ActS' \subseteq \ActS$ and $\INT' \intpr \INT$.
Then, letting $\ActS' = \ActS'_1 \cup \ActS'_2$, 
subtree \eqref{eq:bangaccept} is as follows:
%where (\ref{}) and (\ref{eq:bangrequest}) correspond to the subtrees:
\begin{equation}\label{eq:bangaccept}
	\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\repopen{a}{x}.P_1\}}{\type{\ActS_1'}{ \INT_1'\addelta a:\ST_\quau }}}		  
    { \judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1}{ \INT'_1\addelta a:\ST_\quau}} & 
    	\infer{\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P_1}{\type{\emptyset}{\,\unres(\INT_1)\addelta a:\ST_\quau }}}
  {\Gamma \vdash a: \langle \ST_\quau , \overline{\ST }_\qual \rangle &
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{x:\ST}{\INT_1}} }}
\end{equation}
with 
\begin{equation}
\jug_1 = \Gamma; \Theta \vdash \type{\emptyset}{\,\unres(\INT_1)\addelta a:\ST_\quau} \label{eq:srjugro1}
\end{equation}
Then, subtree \eqref{eq:bangrequest} is as follows:

\begin{equation}\label{eq:bangrequest}
 \infer{\judgebis{\env{\Gamma}{\Theta}}{D\{\nopenr{a}{y}.P_2 \}}{ \type{\ActS'_2}{ \INT'_2\addelta a:\overline{\ST}_{\qual} }}}
	{\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2}{ \INT'_2\addelta a:\overline{\ST}_\qual}}  & \infer{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{y}.P_2}{ \type{\ActS_2}{ \INT_2\addelta a:\overline{\ST}_{\qual} }}}
	{\Gamma \vdash a: \langle \ST_\quau , \overline{\ST}_\qual \rangle &
\judgebis{\env{\Gamma}{\Theta}}{P_2}{\type{\ActS_2, y:\overline{\ST }}{\INT_2}}}
}
\end{equation}
 with 
 \begin{equation}
 \jug_2 = \Gamma; \Theta \vdash \type{\ActS_2}{\INT_2 \addelta a:\overline{\ST}_\qual} \label{eq:srjugro2}
 \end{equation}
\noindent %where\done\todo[B37.]{Fixed, pls check} 
By Lemma~\ref{lem:context} we have  
$\ActS_1 \subseteq \ActS'_1$ and
$\ActS_2 \subseteq \ActS_2'$. Moreover, $\INT_1 \intpr \INT_1'$, $\INT_2 \intpr \INT_2'$ and $\INT' \intpr \INT$.
% where $ \INT' = (\INT'_1 \addelta \inter{a}{\ST}{\infty}) \addelta (\INT'_2\addelta \inter{a}{\overline{\ST}}{1} )$. 
 Now, using Lemma~\ref{lem:substitution}(\ref{subchavar}) on $P_1$ and $P_2$, we have:
 \begin{enumerate}[(a)]
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_1\sub{\cha^+}{x}}{ \type{ \cha^+:\ST}{\INT_1}}$.
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}$.
 \end{enumerate}
 We now describe how to obtain appropriately typed contexts $C^+, D^+$, and $E^{++}$ based on the information inferred up to here
on contexts $C, D$, and $E$. We first describe the case of $C^+$.
From~\eqref{eq:bangaccept} above we obtained
$\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1}{ \INT'_1 \addelta a:\ST_{\quau}}}$
with $\jug_1$ as in \eqref{eq:srjugro1}.
 Then, using Lemma~\ref{l:ctxop}(1), we infer
$\judgebis{\bullet_{\jug_3}; \env{\Gamma}{\Theta}}{C^+}{\type{\ActS'_1, \cha^+:\ST}{ \INT'_1}}$
with 
 \begin{equation}
 \jug_3 =  \Gamma; \Theta \vdash \type{\cha^+:\ST}{\unres(\INT_1)\addelta a:\ST_\quau} \label{eq:srjugro3}
 \end{equation}
We may now reconstruct the derivation given in \eqref{eq:bangaccept}:
\begin{equation}\label{eq:bangacceptsubfin}
\infer{\judgebis{\env{\Gamma}{\Theta}}{C^{+}\{P_{1}\sub{\cha^+}{x}\}}{\type{\ActS_1', \cha^+:\ST}{ \INT_1' \addelta a:\ST_\quau}}}		  
    { \judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{C^+}{\type{\ActS'_1, \cha^+:\ST\,}{ \INT'_1 \addelta a:\ST_\quau}} &  
    	\judgebis{\env{\Gamma}{ \Theta}}{P_{1}\sub{\cha^+}{x}}{ \type{ \cha^+:\ST}{\unres(\INT_1)\addelta a:\ST_\quau}}}
\end{equation}
For $D^+$, we proceed analogously from \eqref{eq:bangrequest} and infer:
\begin{equation}\label{eq:bangrequestsubfin}
 \infer{\judgebis{\env{\Gamma}{\Theta}}{D^{+}\{P_{2}\sub{\cha^-}{y}\}}{\type{\ActS'_2,\cha^- :\overline{\ST } }{\INT'_2}}}
	{\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D^+}{\type{\ActS'_2, \cha^-:\overline{\ST}}{ \INT'_2}} & \judgebis{\env{\Gamma}{ \Theta}}{P_{2}\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}}
\end{equation}
with 
 \begin{equation}
 \jug_4 =  \Gamma; \Theta \vdash \type{\ActS_2, \cha^-:\overline{\ST}}{\INT_2} \label{eq:srjugro4}
 \end{equation}
To infer the type of $E^{++}$ we proceed as before using twice Lemma~\ref{l:ctxop}(1), combined with~\eqref{eq:srjugro0}.
We may finally derive the type for the result of the reduction: using rules \rulename{t:Par}, \rulename{t:CRes}, and \rulename{t:Fill} we obtain:
$$
\infer
{\judgebis{\env{\Gamma}{\Theta}}{E^{++}_{} \big\{\restr{\cha}{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\}} \big\} }{\type{\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT''}}}
{\eqref{eq:banglast}   &
	\infer{\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\}}}{\type{\ActS', [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT_1' \addelta \INT_2'\addelta a:\ST_\quau}}}
{\infer{\judgebis{\env{\Gamma}{\Theta}}{{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\} }}{\type{\ActS', \cha^+:\ST, \cha^-:\overline{\ST} }{ \INT_1' \addelta \INT_2'\addelta a:\ST_\quau}}}{
\eqref{eq:bangacceptsubfin}
%
&
%
	\eqref{eq:bangrequestsubfin}
}
}}
$$
with 
 \begin{equation}\label{eq:banglast}
\judgebis{\bullet_{\jug_5} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]}{ \INT'' }}
 \end{equation}
and 
$$
 \jug_5 =  \Gamma; \Theta \vdash \type{\ActS', \cha^+:\ST, \cha^-:\overline{\ST} }{ \INT_1' \addelta \INT_2'\addelta a:\ST_\quau}
$$
Notice that by Lemma \ref{lem:context}, we have $\INT'' \intpr \INT_1' \cup \INT_2'\addelta a:\ST_\quau$.
Also, observe that by assumption $\ActS$ is balanced; therefore, 
by Def.~\ref{d:balanced}
the resulting typing $\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]$ is balanced too.
This concludes this case. 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\paragraph{\bf Case \rulename{r:Upd}} From Table~\ref{tab:semantics} we have:
$$E\big\{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{\mathsf{X}}\}\big\} 
\pired   
E_{}\big\{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}\big\}$$
By assumption we have $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{\mathsf{X}}\}\big\}}{ \type{\ActS}{\INT}}$,
with $\ActS$ balanced.
Then, by inversion on typing, using rules
%is obtained by the following derivation tree using Lemma \ref{lem:context} ($\Leftarrow$) and  inversion on rules 
\rulename{t:Fill}, \rulename{t:Par}, \rulename{t:Adapt}, and \rulename{t:Loc} we infer:
\begin{equation}\label{eq:srupd00}
\infer
{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{\mathsf{X}}\}\big\}}{ \type{\ActS}{\INT}}}
{\judgebis{\bullet_{\jug_0} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{ \INT }}  & \infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{\mathsf{X}}\}}{ \type{\ActS'}{\INT'}}}
{
\eqref{eq:srupd0}
&
\eqref{eq:srupd1}
}}
\end{equation}
with
$\jug_0 =  \Gamma; \Theta \vdash \type{\ActS'}{\INT'}$.
By Lemma~\ref{lem:context}, we have
$\ActS' \subseteq \ActS'$ and $\INT' \intpr \INT$.
Moreover, 
letting $\ActS' = \ActS'_1 \cup \ActS'_2$ and $\INT' = \INT'_1 \addelta \INT'_2$, 
subtree \eqref{eq:srupd0} is as follows:
\begin{equation}\label{eq:srupd0}
\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\component{l}{0}{}{P_1}\} }{ \type{\ActS'_1}{\INT'_1}}}
{\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1}{ \INT'_1 }}  & \infer{\judgebis{\env{\Gamma}{\Theta}}{\compo{l}{0}{P_1}}{ \type{\emptyset}{\INT''_1}}}
{ \INT''_1 \intpr \INT^*_1 & \Theta \vdash l:\INT^*_1
  & \judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\emptyset}{\INT''_1} }   }}
\end{equation}
with
$\jug_1 =  \Gamma; \Theta \vdash \type{\emptyset}{\INT''_1}$,
and $\INT''_1 \intpr \INT'_1$ (by Lemma~\ref{lem:context}).
Subtree \eqref{eq:srupd1} is as follows:
\begin{equation}\label{eq:srupd1}
\infer{\judgebis{\env{\Gamma}{\Theta}}{D\{\adapt{l}{P_2}{\mathsf{X}}\}}{ \type{\ActS'_2}{\INT'_2}}}{
\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2}{ \INT'_2 }} & 
\infer{\judgebis{\env{\Gamma}{\Theta}}{ \adapt{l}{P_2}{\mathsf{X}}}{ \type{\emptyset}{\emptyset}}}
{\Theta \vdash l:\INT^*_1  &  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT^*_1}}}{P_2}{\type{\emptyset}{ \INT_3 }}}}
\end{equation}
with
$\jug_2 =  \Gamma; \Theta \vdash \type{\emptyset}{\emptyset}$.
%By Lemma \ref{lem:context} ($\Leftarrow$) we have $\ActS_1 \cup \ActS_2 \subseteq \ActS$, $\INT_2 \intpr \INT_2'$, $\INT_4 \intpr \INT_4'$, and $\INT_2' \addelta \INT_4' \intpr \INT$. 
By Lemma~\ref{lem:substitution}(\ref{subprovar}) we have  $\judgebis{\env{\Gamma}{\Theta}}{ P_2\sub{P_1}{\mathsf{X}}}{\type{\emptyset}{\INT'_3}}$,
for some $\INT'_3$ such that $\INT'_3 \intpr \INT_3$.
We now reconstruct the derivation in \eqref{eq:srupd00}, using rules
\rulename{t:Par}, \rulename{t:Fill} and Lemma~\ref{l:ctxop}(3). Let
%, thus process $E_{}\big\{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}\big\}$ can be typed by means of Lemma~\ref{lem:context} ($\Rightarrow$) and rule \rulename{t:Par}:
\begin{equation}\label{eq:finupd}
\infer
{\judgebis{\env{\Gamma}{\Theta}}{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}}{ \type{\ActS'_1 \cup \ActS'_2}{\INT''_3 \addelta \INT_2'}}}
{\infer{\judgebis{\env{\Gamma}{\Theta}}{ C\{P_2\sub{P_1}{\mathsf{X}}\} }{\type{\ActS'_1}{\INT''_3}}}{
\judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_1'}{ \INT_3'' }} &
\judgebis{\env{\Gamma}{\Theta}}{ P_2\sub{P_1}{\mathsf{X}}}{\type{\emptyset}{\INT'_3}}}
&
\infer{\judgebis{\env{\Gamma}{\Theta}}{D\{\nil\}}{ \type{\ActS'_2}{\INT'_2}}}{
\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_2'}{ \INT_2' }}
&\judgebis{\env{\Gamma}{\Theta}}{\nil}{ \type{\emptyset}{\emptyset}}}
}
\end{equation}
and
$$
\infer{\judgebis{\env{\Gamma}{\Theta}}{E_{}\big\{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}\big\}}{ \type{\ActS}{\INT'}}}
{\judgebis{\bullet_{\jug_5} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{\INT'}}
&\eqref{eq:finupd}}
$$
with
$$
\begin{array}{c}
\jug_5 =  \Gamma; \Theta \vdash \type{\ActS'_1 \cup \ActS'_2}{\INT''_3 \addelta \INT'_2}
 \end{array}
$$
where by Lemma \ref{lem:context} %($\Rightarrow$) 
we know $\INT_3'' \intpr \INT'_3$ and $\INT_3'' \addelta \INT_2' \intpr \INT'$.
This concludes the analysis for this case.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\paragraph{\bf Case \rulename{r:I/O}} From Table~\ref{tab:semantics} we have:
$$E\big\{C\{\outC{\cha^{\,p}}{\til{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\til{x}}.P_2\}\big\} 
\pired 
E\big\{C\{P_1\} \para  D\{P_2\sub{\til{c}\,}{\til{x}}\}\big\} \quad (\til{e} \downarrow \til{c})$$
By assumption, we have $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\outC{\cha^{\,p}}{\til{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\til{x}}.P_2\}\big\} }{ \type{\ActS}{\INT}}$, with $\ActS$ balanced.
By inversion on typing, using rules 
%we obtain the following derivation that employs Lemma~\ref{lem:context} ($\Leftarrow$) three times and inversion on rules  
\rulename{t:Fill}, \rulename{t:Par}, \rulename{t:In}, and \rulename{t:Out}, we infer:
%$$
%R \triangleq C\{\outC{\cha^{\,p}}{\til{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\til{x}}.P_2\}
%$$
$$
\infer{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\outC{\cha^{\,p}}{\til{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\til{x}}.P_2\}\big\} }{ \type{\ActS}{\INT}}}
{\judgebis{\bullet_{\jug_0} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{\INT}} & \infer
{
\judgebis{\env{\Gamma}{\Theta}}{C\{\outC{\cha^{\,p}}{\til{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\til{x}}.P_2\}} {\type{\ActS'}{ \INT_1' \addelta \INT_2'}}}
{ \eqref{eq:out}
&
\eqref{eq:in}
}}
$$
where:
\begin{eqnarray}
\ActS' & = & \ActS_1' \cup \ActS_2', \cha^p:!(\til{\capab}).{\ST}, \cha^{\overline{p}}:?(\til{\capab}).\overline{\ST} \\
\INT & = & \INT_1' \addelta \INT_2' \\
\jug_0 & = &   \Gamma; \Theta \vdash \type{\ActS'}{\INT'_1 \addelta \INT'_2}
\end{eqnarray}
Moreover, by Lemma~\ref{lem:context}, we infer $\ActS' \subseteq \ActS$ and $\INT'_1 \addelta \INT'_2 \intpr \INT$.
Also, we have that subtree \eqref{eq:out} is as follows:
\begin{equation}\label{eq:out} 
\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\outC{\cha^{p}}{\til{e}}.P_1\} } {\type{\ActS_1',  \cha^p:!(\til{\capab}).{\ST} }{ \INT_1' }}}{
\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_1}{ \INT'_2 }} &   \infer
{\judgebis{\env{\Gamma}{\Theta}}{\outC{\cha^p}{\til{e}}.P_1}{\type{\ActS_1, \cha^p:!(\til{\capab}).{\ST}}{ \INT_1}}}
{\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1, \cha^p:{\ST}}{ \INT_1}} & \Gamma \vdash \til{e}:\til{\capab}}}
\end{equation}
with
$$
 \jug_1 =  \Gamma; \Theta \vdash \type{\ActS_1, \cha^p:!(\til{\capab}).{\ST}}{ \INT_1}
$$
Also, subtree \eqref{eq:in} is as follows:
\begin{equation}\label{eq:in}
 \infer{\judgebis{\env{\Gamma}{\Theta}}{ D\{\inC{\cha^{\overline{p}}}{\til{x}}.P_2\}}{\type{ \ActS_2', \cha^{\overline{p}}:?(\til{\capab}).\overline{\ST}}{ \INT_2'}}}
{\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_1}{ \INT'_2 }} & 
  \infer
{\judgebis{\env{\Gamma}{\Theta}}{\inC{\cha^{\overline{p}}}{\til{x}}.P_1 }{\type{\ActS_2, \cha^{\overline{p}}:?(\til{\capab}).\overline{\ST}}{ \INT_2}}}
{\judgebis{\env{\Gamma, \til{x}:\til{\capab}}{\Theta}}{P_2}{\type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{\INT_2}}}}
\end{equation}
with
$$
 \jug_2 =  \Gamma; \Theta \vdash \type{\ActS_2, \cha^{\overline{p}}:?(\til{\capab}).\overline{\ST}}{ \INT_2}
$$
where Lemma~\ref{lem:context}  ensures $\ActS_1 \subseteq \ActS_1'$, $\ActS_2 \subseteq \ActS_2'$, $\ActS \subseteq \ActS_1' \cup \ActS_2', \cha^p:!(\til{\capab}).{\ST}, \cha^{\overline{p}}:?(\til{\capab}).\overline{\ST} $, $\INT_1 \intpr \INT_1'$, $\INT_2 \intpr \INT_2'$, and $ \INT \intpr \INT_1 \uplus \INT_2$.

Now, by Lemma \ref{lem:substitution}(2)  we know $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\til{c}}{\til{x}}}{\type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{\INT_2}}$ with $\til{e} \downarrow \til{c}$. Moreover by Lemma \ref{l:ctxop}(3) and  rules \rulename{t:Par} and \rulename{t:Fill} we obtain the following type derivations:
\begin{equation}\label{eq:output}
\infer{\judgebis{\env{\Gamma}{ \Theta}}{C\{P_1\}}{\type{\ActS_1', \cha^p:\ST}{\INT_1'}}}
{\judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_1', \cha^p:\ST}{\INT_1'}} 
&
\judgebis{\env{\Gamma}{ \Theta}}{P_1}{\type{\ActS_1, \cha^p:\ST}{\INT_1}}}
\end{equation}
\begin{equation}\label{eq:input}
 \infer{\judgebis{\env{\Gamma}{\Theta}}{D\{P_2\sub{\til{c}\,}{\til{x}}\}}{\type{\ActS_2', \cha^{\overline{p}}:\overline{\ST}}{ \INT_2'}}}{
\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_2', \cha^{\overline{p}}:\overline{\ST}}{ \INT_2'}} 
& \judgebis{\env{\Gamma}{\Theta}}{P_2\sub{\til{c}\,}{\til{x}}}{\type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{ \INT_2}} }
\end{equation}

 $$
\infer{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{P_1\} \para  D\{P_2\sub{\til{c}\,}{\til{x}}\}\big\} }{ \type{\ActS'}{\INT}}}
{\judgebis{\bullet_{\jug_5} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS'}{\INT}}  
 & \infer
{\judgebis{\env{\Gamma}{\Theta}}{C\{P_1\} \para  D\{P_2\sub{\til{c}\,}{\til{x}}\}}{\type{\ActS_1' \cup \ActS_2', \cha^p:\ST, \cha^{\overline{p}}\overline{\ST} }{ \INT_1' \addelta \INT_2'}}}
 {\eqref{eq:output}   & \eqref{eq:input}}
}
$$ 
with
$$
\begin{array}{c}
 \jug_3 =  \Gamma; \Theta \vdash \type{\ActS_1, \cha^p:\ST}{\INT_1}\\
 \jug_4 =  \Gamma; \Theta \vdash \type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{ \INT_2}\\
 \jug_5 =  \Gamma; \Theta \vdash \type{\ActS_1' \cup \ActS_2', \cha^p:\ST, \cha^{\overline{p}}\overline{\ST} }{ \INT_1' \addelta \INT_2'}
\end{array}
$$

Since by inductive hypothesis  $\ActS_1'$ and $\ActS_2'$ are balanced, we infer that  $\ActS_1' \cup \ActS_2', \cha^p:\ST, \cha^{\overline{p}}:\overline{\ST}$ is balanced as well; this concludes the proof for this case.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\paragraph{\bf Case \rulename{r:Pass}} From Table~\ref{tab:semantics} we have:
$$E\big\{C\{\throw{\cha^{\,p}}{\cha_1^{\,q}}.P_1\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.P_2\}\big\}\pired E\big\{C^{-}\{P_1\} \para  D^{+}\{P_2\sub{\cha_1^{\,q}}{x}\}\big\}$$

By assumption we have  $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\throw{\cha^{\,p}}{\cha_1^{\,q}}.P_1\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.P_2\}\big\}}{ \type{\ActS}{\INT}}$, with $\ActS$ balanced. 
By typing inversion on rules 
%Using   Lemma \ref{lem:context} ($\Leftarrow$) and inversion on rules 
\rulename{t:Fill},
\rulename{t:Par}, \rulename{t:Cat}, and \rulename{t:Thr} we infer:
$$
\infer
	{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\throw{\cha^{\,p}}{\cha_1^{\,q}}.P_1\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.P_2\}\big\}}{ \type{\ActS}{\INT}}}
{\judgebis{\bullet_{\jug_0} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{\INT}} & \infer
	{\judgebis{\env{\Gamma}{\Theta}}{C\{\throw{\cha^{p}}{\cha_1^{q}}.P_1\} \para  D\{\catch{\cha^{\overline{p}}}{x}.P_2\}}{ \type{\ActS'}{\INT'}}}
	{
	\eqref{eq:throw}
	&
	\eqref{eq:catch}
	}}
$$
 with: 
 \begin{eqnarray}
 \ActS & = & \ActS_1, \cha^p:!(\ST).\overline{\STT}, \cha_1^{q}:\ST, \ActS_2, \cha^{\overline{p}}:?(\ST).\STT \\
 \ActS' & = & \ActS'_1, \cha^p:!(\ST).\overline{\STT}, \cha_1^{q}:\ST, \ActS'_2, , \cha^{\overline{p}}:?(\ST).\STT \\
 \jug_0 & = &  \Gamma; \Theta \vdash \type{\ActS'}{\INT'} \label{eq:srjugps2}
 \end{eqnarray}
 and, by Lemma~\ref{lem:context}, we infer $\ActS'_1 \subseteq \ActS_1$, $\ActS'_2 \subseteq \ActS_2$, and $\INT' \intpr \INT$.
 Moreover, \eqref{eq:throw}  corresponds to the subtree:
\begin{equation}\label{eq:throw}
 \infer
		{\judgebis{\env{\Gamma}{\Theta}}{C\{\throw{\cha^{p}}{\cha_1^{q}}.P_1\} }{ \type{\ActS'_1, \cha^p:!(\ST).\overline{\STT}, \cha_1^{q}:\ST}{ \INT'_1}}}
		{\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1, \cha^p:!(\ST).\overline{\STT},\, \cha_1^{q}:\ST}{ \INT'_1 }}  & \infer
{\judgebis{\env{\Gamma}{\Theta}}{\throw{\cha^p}{\cha_1^{q}}.P_1}{\type{\ActS''_1,\, \cha^p:!(\ST).\overline{\STT},\, \cha_1^{q}:\ST}{ \INT''_1}}}
{\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS''_1, \cha^p:\overline{\STT}}{ \INT''_1}} 
		}}
\end{equation}
with $\ActS''_1 \subseteq \ActS'_1$ and $\INT''_1 \intpr \INT'_1$ (by Lemma~\ref{lem:context}) and
 \begin{eqnarray}
 \jug_1 & = &  \Gamma; \Theta \vdash \type{\ActS''_1,\, \cha^p:!(\ST).\overline{\STT},\, \cha_1^{q}:\ST}{\INT''_1} \label{eq:srjugps3}
 \end{eqnarray}
while \eqref{eq:catch}   corresponds to the subtree:
\begin{equation}\label{eq:catch}
 \infer
		{\judgebis{\env{\Gamma}{\Theta}}{ D\{\catch{\cha^{\overline{p}}}{x}.P_2\}}{ \type{\ActS'_2, \cha^{\overline{p}}:?(\ST).\STT}{ \INT'_2}}}
		{\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2, \cha^{\overline{p}}:?(\ST).\STT}{ \INT'_2 }} & \infer
{\judgebis{\env{\Gamma}{\Theta}}{\catch{\cha^{\overline{p}}}{x}.P_2 }{\type{\ActS''_2, \cha^{\overline{p}}:?(\ST).\STT}{\INT''_2}}}
{\judgebis{\env{\Gamma}{\Theta}}{P_2}{\type{\ActS''_2, \cha^{\overline{p}}:\STT, x:\ST}{\INT''_2}}}	
}
\end{equation}
with $\ActS''_2 \subseteq \ActS'_2$ and $\INT''_2 \intpr \INT'_2$ (by Lemma~\ref{lem:context}) and
 \begin{eqnarray}
 \jug_2 & = &  \Gamma; \Theta \vdash \type{\ActS''_2, \cha^{\overline{p}}:?(\ST).\STT}{\INT''_2} \label{eq:srjugps4}
 \end{eqnarray}
%
%and where by Lemma \ref{lem:context} ($\Leftarrow$) ensures $\ActS_1 \subseteq \ActS_1'$, $\ActS_2 \subseteq \ActS_2'$, $\ActS' \subseteq \ActS$ and $\ActS' = \ActS'_1 \cup \ActS'_2,  \cha^p:!(\ST).\overline{\STT}, \cha_1^q:\ST, \cha^{\overline{p}}:?(\ST).\STT$. Moreover we have $\INT_1 \intpr \INT_1'$, $\INT_2 \intpr \INT_2'$, $\INT' \intpr \INT$ and $\INT' = \INT'_1 \addelta \INT'_2$. Notice that as $\ActS$ is balanced, in $\ActS$ there is a $\cha_1^{\overline{q}}:\overline{\ST}$.

We now describe how to obtain appropriately typed contexts $C^-$ and $D^+$, 
based on the information already inferred  on contexts $C$ and $D$.
We first consider the case of $C^-$. From \eqref{eq:throw}, we obtained 
$$
\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1, \cha^p:!(\ST).\overline{\STT},\, \cha_1^{q}:\ST}{ \INT'_1 }}
$$
with $\jug_1$ as in \eqref{eq:srjugps3}. Then, using Lemma~\ref{l:ctxop}(2), we infer 
$$
\judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{C^-}{\type{\ActS'_1, \cha^p:\overline{\STT}}{ \INT'_1 }}
$$
where 
 \begin{eqnarray}
 \jug_3 & = &  \Gamma; \Theta \vdash \type{\ActS''_1,\, \cha^p: \overline{\STT} }{\INT''_1}  \label{eq:srjugps5}
 \end{eqnarray}
We may now reconstruct the derivation in~\eqref{eq:throw}, as follows:
\begin{equation}\label{eq:passd}
\infer
		{\judgebis{\env{\Gamma}{\Theta}}{C^{-}\{P_1\} }{ \type{\ActS'_1, \cha^p:\overline{\STT}}{ \INT'_1}}}
		{\judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{C^-}{\type{\ActS'_1, \cha^p:\overline{\STT}}{ \INT'_1 }} &\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS''_1, \cha^p:\overline{\STT}}{ \INT''_1}} 
		}
\end{equation}
We now consider the case of $D^+$.
By applying Lemma \ref{lem:substitution} \eqref{subchavar}
on the premise concerning $P_2$ in \eqref{eq:catch}, we obtain
$$\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha_1^q}{x}}{\type{\ActS''_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{ \INT''_2}}$$ 
From \eqref{eq:catch} we obtained
$$
\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2, \cha^{\overline{p}}:?(\ST).\STT}{ \INT'_2 }}
$$
with $\jug_2$ as in \eqref{eq:srjugps4}. Then, using Lemma~\ref{l:ctxop}(1), we infer 
$$
\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D^+}{\type{\ActS'_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{ \INT'_2 }}
$$
where
 \begin{eqnarray}
 \jug_4 & = &  \Gamma; \Theta \vdash \type{\ActS''_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{\INT''_2} \label{eq:srjugps6}
 \end{eqnarray}
We can reconstruct the derivation depicted by \eqref{eq:catch}:
%thus obtaining the following typing tree where we have used Lemma \ref{lem:context} ($\Rightarrow$) and rule \rulename{t:Par}, we also use the following subtree:
\begin{equation}\label{eq:pass}
 \infer
		{\judgebis{\env{\Gamma}{\Theta}}{ D^{+}\{P_2\sub{\cha_1^{q}}{x}\}}{ \type{\ActS'_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{ \INT'_2}}}
		{\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D^+}{\type{\ActS'_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{ \INT'_2 }} & \judgebis{\env{\Gamma}{\Theta}}{P_2\sub{\cha_1^{q}}{x}}{\type{\ActS''_2, \cha^+:\STT, \cha_1^q:\ST}{\INT''_2}}	
}
\end{equation}
Combining 
\eqref{eq:passd} and \eqref{eq:pass}, 
we may finally derive the type for the result of the reduction. Using rules \rulename{T:Par}  and \rulename{T:Fill} we obtain:
$$
\infer
	{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C^{-}\{P_1\} \para  D^{+}\{P_2\sub{\cha_1^{q}}{x}\}\big\}}{ \type{\ActS^*}{\INT}}}
{\judgebis{\bullet_{\jug_5} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS^*}{\INT}}
 & \infer
	{\judgebis{\env{\Gamma}{\Theta}}{C^{-}\{P_1\} \para  D^{+}\{P_2\sub{\cha_1^{q}}{x}\}}{ \type{\ActS'_1 \cup \ActS'_2, \cha^p:\overline{\STT}, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{\INT'}}}
	{\eqref{eq:passd} & \eqref{eq:pass}
	}}
$$
with
$$
\jug_5 =  \Gamma; \Theta \vdash \type{\ActS'_1 \cup \ActS'_2, \cha^p:\overline{\STT}, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{\INT'}
$$
Since by assumption $\ActS$ is balanced, we have that 
by construction $\ActS^*$ is balanced as well. It is worth observing how contexts $C^{-}$ and $D^{+}$ correctly implement the fact that the number of active sessions is changed after delegating session $\kappa_1^{q}$ to process $P_2$.
 This concludes the proof for this case.


% 
\paragraph{\bf Cases \rulename{r:IfTr} and \rulename{r:IfFa}} Follows by an ease induction on the derivation tree.

% 
\paragraph{\bf Case \rulename{r:Close}} These follow by the same reasoning as in  \rulename{r:Open} case.
% 
\paragraph{\bf Case \rulename{r:Branch}} This case is similar to  previous \rulename{r:I/O} case. 
% 
\paragraph{\bf Case \rulename{r:Str}} Follows from Theorem~\ref{th:congr} (Subject Congruence).
% 
\paragraph{\bf Case \rulename{r:Par}} Follows by induction and by applying rule $\rulename{t:Par}$.
%
\paragraph{\bf Case \rulename{r:Res}} Follows by induction and by the fact that  $\ActS$ is balanced. Indeed, by hypothesis and by inversion on rule \rulename{t:CRes} all the occurences of bracketed assignements ($[\cha^p:\ST]$) are necessarily balanced thus making it possible to apply the inductive hypothesis to the premise of the rule and concluding the analysis of this case and the proof of the theorem.
% \end{description}
\end{proof}



\section{Additional Material for \S\,\ref{sec:disc}\label{ap:addmat}}
\begin{table}[t]
{
$$
\begin{array}{ll}
 \rulename{r:LPar} & \text{if } P \pired P' ~~\text{then} ~~ P \para Q \pired P' \para Q  \vspace{2mm}
\\
 \rulename{r:LRes} &
\text{if } P \pired P' ~~\text{then} ~~ \restr{\cha}{P} \pired \restr{\cha}{P'} %\vspace{2mm} \\
\vspace{2.0mm} \\
 \rulename{r:LStr} &
\text{if } P \equiv P',\, P' \pired Q', \,\text{and}\, Q' \equiv Q ~\text{then} ~ P \pired Q \vspace{2mm}
\\
  \rulename{r:LLoc} &
 \text{if } P \pired P'~~\text{then}~~ \scomponent{l}{P} \pired \scomponent{l}{P'} \vspace{2mm}
 \\ 
 \rulename{r:LOpen} & 
C\{\nopena{a}{x}.P\} \para  D\{\nopenr{a}{y}.Q\} \pired  \\
& 
\hfill \restr{\cha}{\big({C\{P\sub{\cha^+}{x}\}  \para  D\{Q\sub{\cha^-}{y}\} }\big) } \vspace{2.0mm} \\
\rulename{r:LROpen} & 
C\{\repopen{a}{x}.P\}  \para  D\{\nopenr{a}{y}.Q\}   \pired  \\
& 
\hfill \restr{\cha}{\big({C\{P\sub{\cha^+}{x}  \para \repopen{a}{x}.P \}  \para  D\{Q\sub{\cha^-}{y}\} }\big)} 
 \vspace{2.0mm}\\
\rulename{r:LUpd} & 
C\{\component{l}{}{}{P}\} \para  D\{\adapt{l}{Q}{X}\} 
\pired   %\\
%& \hfill 
C\{Q\sub{P}{\mathsf{X}}\}  \para  D\{\nil\} \vspace{2mm} \\

\rulename{r:LI/O} &
C\{\outC{\cha^{\,p}}{\widetilde{e}}.P\} \para  D\{\inC{\cha^{\,\overline{p}}}{\widetilde{x}}.Q\}
\pired %\\
%& \hfill 
C\{P\} \para  D\{Q\sub{\widetilde{c}\,}{\widetilde{x}}\} \quad (\widetilde{e} \downarrow \widetilde{c}) \vspace{2mm}
\\
\rulename{r:LPass} &
C\{\throw{\cha^{\,p}}{\cha'^{\,q}}.P\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.Q\}\pired  C\{P\} \para  D\{Q\sub{\cha'^{\,q}}{x}\} %\\
%& \hfill E\big\{C^{-}\{P\} \para  D^{+}\{Q\sub{\cha'^{\,q}}{x}\}\big\} 
\vspace{2mm}
\\
\rulename{r:LSel} &
C\{\branch{\cha^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m}\} \para  D\{\select{\cha^{\,\overline{p}}}{n_j};Q\} 
\pired \\
& 
\hfill C\{P_j\}\para  D\{Q\}  \quad (1 \leq j \leq m)  \vspace{2mm}
\\
\rulename{r:LClose} &
C\{\close{\cha^{\,p}}.P\} \para  D\{\close{\cha^{\,\overline{p}}}.Q\} \pired %\\
%& \hfill 
C\{P\} \para  D\{Q\} \vspace{ 2mm}
\\
\rulename{r:LIfTr} &
\ifte{e}{P}{Q} \pired P  \quad (e \downarrow \mathtt{true})  \vspace{2mm}
\\
 \rulename{r:LIfFa} &
\ifte{e}{P}{Q} \pired Q  \quad (e \downarrow \mathtt{false}) \vspace{2mm}
\end{array}
$$
}
\caption{Reduction semantics without annotations. } \label{tab:semanticsnoannot}
\end{table}




 \begin{table}[t]
 $$
 \begin{array}{lc}
 \rulename{r:ParU} &
 \infer{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{ \type{\ActS_1 \cup \ActS_2}{\INT_1 \cup \INT_2 }} \pired \judgebis{\env{\Gamma}{\Theta}}{P' \para Q}{ \type{\ActS_1' \cup \ActS_2}{\INT_1' \uplus \INT_2' }}}{ \judgebis{\env{\Gamma}{\Theta}}{P }{ \type{\ActS_1}{\INT_1 }} \pired \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS_1'}{\INT_1' }}}
  \\ \\ 
 \rulename{r:ResU} &
 \infer{
 \begin{array}{c}
 \judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{P}}{ \type{[\cha^+:\alpha], [\cha^-:\overline{\alpha}],\ActS}{\INT }} \pired \\
 \judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{P'} }{ \type{[\cha^+:\alpha'],[ \cha^-:\overline{\alpha'}],\ActS' }{\INT'  }}
 \end{array}
 }
 {\judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\cha^+:\alpha, \cha^-:\overline{\alpha},\ActS}{\INT }} \pired \judgebis{\env{\Gamma}{\Theta}}{P' }{\type{\cha^+:\alpha', \cha^-:\overline{\alpha'},\ActS'}{\INT' }}}
 \\ \\
 \rulename{r:StrU} &
 \infer{\judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS}{\INT }} \pired \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS'}{\INT'}}}{P \equiv Q \quad \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS}{\INT }} \pired \judgebis{\env{\Gamma}{\Theta}}{Q'}{ \type{\ActS'}{\INT'}} \quad  P' \equiv Q'}
  \\ \\
  \rulename{r:LocU} &
 \infer{\judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P}}{ \type{\ActS}{\INT }} \pired \judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P'}}{ \type{\ActS'}{\INT'}}}{\judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS}{\INT }} \pired \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS'}{\INT'}} }
 \\ \\
 \rulename{r:UpdU} &
\infer{
\begin{array}{c}
\judgebis{\env{\Gamma}{\Theta}}{C\{\scomponent{l}{P}\} \para  D\{\adapt{l}{Q}{X}\}}{\type{\ActS}{\INT}}
\\
\pired \\ 
 \judgebis{\env{\Gamma}{\Theta}}{C\{\rho(Q)\sub{P}{\mathsf{X}}\}  \para  D\{\nil\}}{\type{\ActS}{(\INT \setminus \INT_1) \uplus \INT_2}}
\end{array}
}
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{\INT_1}} \quad \judgebis{\env{\Gamma}{\Theta, \mathsf{X}:\ActS_1,\INT_1}}{Q}{\type{\ActS_2}{\INT_2}} \quad \ActS_1 = \rho(\ActS_2)}
 \\ \\
  \rulename{r:IfTrU} &
 \judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{ \type{\ActS}{\INT}}  \pired \judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS}{\INT}} \quad (e \downarrow \mathtt{true}) \vspace{0.2cm}  
 \\ 
  \rulename{r:IfFaU} &
 \judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{ \type{\ActS}{\INT}}  \pired \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS}{\INT}} \quad (e \downarrow \mathtt{false})  
 \end{array}
 $$
 \caption{Typed reduction semantics. (I)}\label{tab:1typedsemantics} 
\end{table}

 
 \begin{table}[t]
  $$
  \begin{array}{l}
 \rulename{r:OpenU} \\ 
 \judgebis{\env{\Gamma}{\Theta}}{C\{\nopena{a}{x}.P\} \para D\{\nopenr{a}{y}.Q\}}{ \type{\ActS}{\INT, a:\alpha_{\qual}, a:\overline{\alpha}_{\qual} }}  \pired \\
  \hfill \judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{C\{P\sub{\cha^+}{x}\} \para D\{Q\sub{\cha^-}{y}}\}}{ \type{\ActS,[\cha^+:\alpha],[\cha^-:\overline{\alpha}]}{\INT}}
 \\ \\ 
 \rulename{r:ROpenU} \\ 
 \judgebis{\env{\Gamma}{\Theta}}{C\{\repopen{a}{x}.P\} \para D\{\nopenr{a}{y}.Q\}}{ \type{\ActS}{\INT, a:\alpha_{\quau}, a:\overline{\alpha}_{\qual} }}  \pired
  \\   \hfill \judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{C\{P\sub{\cha^+}{x} \para \repopen{a}{x}.P\}\para D\{Q\sub{\cha^-}{y}}\}}{ \type{\ActS,[\cha^+:\alpha],[\cha^-:\overline{\alpha}]}{\INT,a:\alpha_{\quau}}}
 \\ \\
  \rulename{r:I/OU} \\
 \judgebis{\env{\Gamma}{\Theta}}{C\{\outC{\cha^{\,p}}{\widetilde{e}}.P\} \para D\{\inC{\cha^{\,\overline{p}}}{\widetilde{x}}.Q\}}{ \type{\ActS,\cha^{p}:!(\tilde{\capab}).\ST, \cha^{\overline{p}}:?(\tilde{\capab}).\overline{\ST}}{\INT}}  \pired \\
  \hfill \judgebis{\env{\Gamma}{\Theta}}{C\{P\} \para D\{Q \sub{\widetilde{c}\,}{\widetilde{x}}\}}{ \type{\ActS,\cha^{p}:\ST, \cha^{\overline{p}}:\overline{\ST}}{\INT}}
 \\ \\
  \rulename{r:PassU} \\
 \judgebis{\env{\Gamma}{\Theta}}{C\{\throw{\cha^{\,p}}{\cha'^{\,q}}.P\} \para D\{\catch{\cha^{\,\overline{p}}}{x}.Q\}}{ \type{\ActS,\cha^{p}:!(\ST).\STT,\cha'^{q}:\ST, \cha^{\overline{p}}:?(\ST).\overline{\STT}}{\INT}}  \pired \\
  \hfill \judgebis{\env{\Gamma}{\Theta}}{C\{P\} \para D\{Q\sub{\cha'^{\,q}}{x}\}}{ \type{\ActS,\cha^{p}:\STT, \cha^{\overline{p}}:\overline{\STT}, \cha'^{q}:\ST}{\INT}}
 \\ \\
  \rulename{r:SelU} \\
 \judgebis{\env{\Gamma}{\Theta}}{C\{\branch{\cha^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m}\} \para  D\{\select{\cha^{\,\overline{p}}}{n_j};Q\}}{
 \\  \type{\ActS,\cha^{p}:\&\{n_1{:}\ST_1, \ldots, n_k{:}\ST_m \}, \cha^{\overline{p}}:\oplus\{n_1:\overline{\ST_1}, \ldots,  n_m:\overline{\ST_m} \} }{\INT}}  \pired \\
  \hfill \judgebis{\env{\Gamma}{\Theta}}{C\{P_j\} \para D\{Q\} }{ \type{\ActS,\cha^{p}:\ST_j, \cha^{\overline{p}}:\overline{\ST_j}}{\INT}}
 \\ \\
  \rulename{r:CloseU} \\
 \judgebis{\env{\Gamma}{\Theta}}{C\{\close{\cha^{\,p}}.P\} \para D\{\close{\cha^{\,\overline{p}}}.Q\}}{ \type{\ActS,\cha^{p}:\epsilon, \cha^{\overline{p}}:\epsilon}{\INT}}  \pired \\
  \hfill \judgebis{\env{\Gamma}{\Theta}}{C\{P\} \para D\{Q\} }{ \type{\ActS}{\INT}}
 \end{array}
 $$
 \caption{Typed reduction semantics. (II)}\label{tab:typedsemantics} 
 \end{table}






\end{document}